Polymonadic Programming

TL;DR

This paper introduces polymonads, a generalization of monads that allows for composing computations with three different effects, providing a flexible framework for effectful programming in functional languages.

Contribution

It formalizes polymonads, demonstrates their expressiveness, and develops a core language with type inference and elaboration supporting polymonadic programming.

Findings

Polymonads subsume monads and parameterized monads.

Type inference in lambda-PM computes principal types.

Elaborated programs are semantically coherent regardless of bind choices.

Abstract

Monads are a popular tool for the working functional programmer to structure effectful computations. This paper presents polymonads, a generalization of monads. Polymonads give the familiar monadic bind the more general type forall a,b. L a -> (a -> M b) -> N b, to compose computations with three different kinds of effects, rather than just one. Polymonads subsume monads and parameterized monads, and can express other constructions, including precise type-and-effect systems and information flow tracking; more generally, polymonads correspond to Tate's productoid semantic model. We show how to equip a core language (called lambda-PM) with syntactic support for programming with polymonads. Type inference and elaboration in lambda-PM allows programmers to write polymonadic code directly in an ML-like syntax--our algorithms compute principal types and produce elaborated programs wherein the binds appear explicitly. Furthermore, we prove that the elaboration is coherent: no matter which (type-correct) binds are chosen, the elaborated program's semantics will be the same. Pleasingly, the inferred types are easy to read: the polymonad laws justify (sometimes dramatic) simplifications, but with no effect on a type's generality.