### Abstract

These theories contain a formalization of first class type constructors and axiomatic constructor classes for HOLCF. This work is described in detail in the ICFP 2012 paper Formal Verification of Monad Transformers by the author. The formalization is a revised and updated version of earlier joint work with Matthews and White.

Based on the hierarchy of type classes in Haskell, we define classes for functors, monads, monad-plus, etc. Each one includes all the standard laws as axioms. We also provide a new user command, tycondef, for defining new type constructors in HOLCF. Using tycondef, we instantiate the type class hierarchy with various monads and monad transformers.

### License

BSD License

### Topics

- Computer science/Functional programming

### Session Tycon

- TypeApp
- Coerce
- Functor
- Monad
- Monad_Zero
- Monad_Plus
- Monad_Zero_Plus
- Lazy_List_Monad
- Maybe_Monad
- Error_Monad
- Writer_Monad
- Binary_Tree_Monad
- Lift_Monad
- Resumption_Transformer
- State_Transformer
- Error_Transformer
- Writer_Transformer
- Monad_Transformer

## Cite

×

Tycon-AFP

    @article{Tycon-AFP,
      author  = {Brian Huffman},
      title   = {Type Constructor Classes and Monad Transformers},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Tycon.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- Jun 28, 2012 : Isabelle2012