Effect polymorphism in higher-order logic (Q7361663)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Monomorphic_Monad
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Effect polymorphism in higher-order logic |
AFP entry Monomorphic_Monad |
Statements
5 May 2017
0 references
Andreas Lochbihler
0 references
Effect polymorphism in higher-order logic (English)
0 references
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.
0 references
