### Abstract

The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. We show that if a monad is used with values of only one type, this notion can be formalised in HOL. Based on this idea, we develop a library of effect specifications and implementations of monads and monad transformers. Hence, we can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects. We illustrate the usefulness of effect polymorphism with a monadic interpreter for a simple language.

### License

BSD License

### History

February 15, 2018
  added further specifications and implementations of non-determinism; more examples (revision bc5399eea78e)

### Topics

- Computer science/Functional programming

### Session Monomorphic_Monad

- Monomorphic_Monad
- Monad_Overloading
- Interpreter
- Just_Do_It_Examples

### Used by

- CryptHOL

## Cite

×

Monomorphic_Monad-AFP

    @article{Monomorphic_Monad-AFP,
      author  = {Andreas Lochbihler},
      title   = {Effect polymorphism in higher-order logic},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Monomorphic_Monad.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
- May 11, 2017 : Isabelle2016-1