Interactions of (co)monads in Agda

We study interaction laws of monads and comonads in the interactive theorem prover Agda. Effectful computations are modeled as monads, while comonads model computation-running machines. Interaction laws describe how computations may be uniformly run to yield values. We study monads and comonads on an arbitrary monoidal category, assuming properties such as symmetry only if needed. We do not assume any axioms from classical mathematics which are noncomputable or those which would be incompatible with univalence such as choice, LEM or K. Our formalization is carried out using the agda-categories mathematical library. It describes interaction laws for functors in general, as well as between monads and comonads. We describe the monoidal category of functor-functor interaction laws. Furthermore, we prove that monoid objects in the category of functor-functor interaction laws are equivalent to monad-comonad interaction laws. Finally, we develop the end calculus in agda-categories and define the dual endofunctor. In this work, we demonstrate several common computationally motivated examples. We show that the monads involved interact with the expected comonads. We also give examples of the dual. As all formalization is completed in a computable mathematical foundation, this thesis gives a computable theory of computations. This enables future creation of programs which manipulate computations in a verified and general way, for example, compilers or program analyzers.

Author dc:creator

• Calvin Santiago Lee 2000-

Contributors dc:contributor

• Háskólinn í Reykjavík

• Tölvunarfræði
• Meistaraprófsritgerðir
• Forritunarmál
• Computer science
• Programming languages (Electronic computers)

Language dc:language.iso

en

Handle dc:identifier.uri

http://hdl.handle.net/1946/48228

OAI identifier oai:identifier

oai:skemman.is:1946/48228