Strict and Lazy Semantics Of Effects

Producer effects and consumer effects combine in several ways. We show that strictness and laziness arise from a combination of a producer and a consumer effect, and relate this type of combination to distributive laws.

Authors

Andrew K. Hirsch and Ross Tate

Abstract

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.

Publication History

Appeared in ICFP 2018.

Official Version

Technical Report

%d bloggers like this: