Don't Try This at Home: No-Go Theorems for Distributive Laws

Add to your list(s) Download to your calendar using vCal

• Daniel Marsden, University of Oxford
• Friday 14 December 2018, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Jamie Vicary.

Monads appear in many aspects of computer science, for example for structuring functional programs or to model of semantics of computational effects. It is desirable to be able to combine monads, so we can use them in a modular way. 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.

This talk will describe general-purpose techniques for showing when there can be no distributive law between two monads. Two approaches will be discussed. The first widely generalizes ideas from a counterexample attributed to Plotkin, yielding general-purpose theorems that recover the previously known situations in which no distributive law can exist. The second approach is entirely novel, encompassing new practical situations beyond our generalizations of Plotkin’s approach. It negatively resolves the open question of whether the list monad distributes over itself.

This is joint work with Maaike Zwart.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.