Abstract

Beck’s distributive laws provide sufficient conditions under which two monads can be composed, and monads arising from distributive laws have many desirable theoretical properties. Unfortunately, finding and verifying distributive laws, or establishing if one even exists, can be extremely difficult and error-prone.

In this talk I will describe two general-purpose techniques for showing when there can be no distributive law between two monads. The first widely generalizes ideas from a counterexample attributed to Plotkin, yielding general-purpose theorems that recover the known situations in which no distributive law can exist. The second approach is entirely novel, encompassing practical situations beyond the generalisation of Plotkin’s argument, including a negative answer to the open question of whether the list monad distributes over itself. As an illustration of our no-go theorems, I will give an overview of the (im)possibility of distributive laws between members of an extension of the Boom hierarchy; a hierarchy of datatypes well-known to functional programmers.

The work I present is done in collaboration with Dan Marsden. To establish our theorems, we used an algebraic perspective on monads, exploiting a syntactic characterization of distributive laws. This approach is key to generalizing beyond what has been achieved by direct calculations in previous work.