Email Gateway (Aug 22 2022 at 15:28): Email Gateway (Aug 22 2022 at 15:28):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Effect polymorphism in higher-order logic
by Andreas Lochbihler
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.
Enjoy 1/5
Last updated: Apr 25 2024 at 08:20 UTC