Effect Polymorphism in Higher-Order Logic (Proof Pearl)
| Autor: | Andreas Lochbihler |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Equational reasoning
Programming language Computer science HOL 020207 software engineering 0102 computer and information sciences 02 engineering and technology Software_PROGRAMMINGTECHNIQUES computer.software_genre Monad (functional programming) 01 natural sciences Higher-order logic Monad Monad transformer Effects Polymorphism Isabelle/HOL TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics 010201 computation theory & mathematics Artificial Intelligence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering computer Software |
| Zdroj: | Journal of Automated Reasoning, 63 (2) |
| Popis: | The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. I show that if a monad is restricted to values of a fixed type, this notion can be formalised in HOL. Based on this idea, I develop a library of effect specifications and implementations of monads and monad transformers. Hence, I can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects. I illustrate the usefulness of effect polymorphism with a monadic interpreter. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|