internalization and categorical algebra
algebra object (associative, Lie, …)
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Unlike the bind operation of a monad which is of type
a polymonadic bind involves three abstract types:
This notion subsumes monads in the sense that every set of monads and monad morphisms can be encoded using polymonads while obeying the polymonad laws. Moreover, it encompasses the monad-like programming patterns.
(Note that, from a category theoretic perspective, it is more natural to change the order of the arguments to match the form of Kleisli extension, so that the operations are of the form
.)
A polymonad is the data of a collection of unary type constructors cointaining an element , and a bind set containing an element (reverse apply).
It must obey the following polymonad laws:
The first four laws are chosen to generalise monads, and the last two are chosen so that if certain binds can be uniquely defined in terms of other ones, then these must be present in .
Nataliya Guts, Michael Hicks, Nikhil Swamy, Daan Leijen, Gavin Bierman, Polymonads, Extended version of POPL’13 submission [pdf, pdf]
Michael Hicks, Gavin Bierman, Nataliya Guts, Daan Leijen, Nikhil Swamy, Polymonadic Programming, EPTCS 153 79-99 (2014) [arXiv:1406.2060, doi:10.4204/EPTCS.153.7]
Jan Bracker, Henrik Nilsson, Polymonad programming in Haskell, Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming, (2015) 1-12 [doi:10.1145/2897336.2897340]
Last revised on December 12, 2023 at 17:26:32. See the history of this page for a list of all contributions to it.