Strict and Lazy Semantics for Effects
Layering Monads and Comonads

ICFP 2018: [pdf] [pdf w/o appendices] [bibtex] [bibtex-tr] [pptx]

Authors: Andrew K. Hirsch and Ross Tate


Two particularly important classes of effects are those that can be given semantics using a monad and those that can be given semantics using a comonad. Currently, programs with both kinds of effects are usually given semantics using a technique that relies on a distributive law. While it is known that not every pair of a monad and a comonad has a distributive law, it was previously unknown if there were any realistic pairs of effects that could not be given semantics in this manner. This paper answers that question by giving an example of a pair of effects that cannot be given semantics using a distributive law. Our example furthermore is intimately tied to the duality of strictness and laziness. We discuss how to view this duality through the lens of effects.

Questions, Comments, and Suggestions

If you have any questions, comments, or suggestions, please e-mail me. I would be glad to know of any opinions people have or any clarifications I should make.