New Haskell programmers often find themselves “trapped in a monad”. Given a computation of type ‘IO a’, there is no way to get the ‘a’ value “out” of the computation. One can use the monadic ‘bind’ operator to create a new computation based on the old one, but this can lead to an awkward style of programming. Haskell is really two distinct sub languages, where the pure sub language is used to compose computations in the monadic sub-language. When effects need to be added to previously pure code we also need to undertake a big refactoring effort, converting ‘let’ to ‘do’, and ‘map’ to ‘mapM’ and so on.

In this talk I’ll present a practical implementation of a coeffect system that lets us get the ‘a’ out. Given a suspended computation M of type ‘IO a’, ‘run M’ evaluates it, releasing its effect into the context, and producing the value of type ‘a’. Conversely, given a term N of type ‘a’ which would perform an IO effect when evaluated, ‘box N’ suspends its evaluation, returning a value of type ‘IO a’. This idea has been described previously, by both Filinski [1] who named the operators ‘reflect’ and ‘reify’, as well as Pfenning and Davies [2] in the context of lax modal logic.

Although the theory works out, manually inserting ‘run’ and ‘box’ casts into a program is even more annoying than converting ‘let’-expressions to ‘do’-expressions when effects need to be added to pure code. Luckily, there is a way to automatically insert these casts during type checking, so we can write code in a style that assumes implicit effects (like in ML), but with types as nice as in Haskell. This system has recently been implemented in DDC [3] as an extension to Dunfield and Krishnaswami’s bidirectional type checking algorithm [4]. Automatically inserting run and box casts works surprisingly well, and also supports DDC’s approach to type safe freezing, where mutable objects can be converted to immutable ones, without unsafe hacks like ‘unsafeFreezeArray’.

[1] Representing Monads Andrzej Filinski Principles of Programming Languages, 2004.

[2] A Judgmental Reconstruction of Modal Logic Frank Pfenning and Rowan Davies Mathematical Structures in Computer Science, 2000.

[3] The Disciplined Disciple Compiler https://github.com/DDCSF/ddc

[4] Complete and Easy Bidirectional Typechecking for Higher-Ranked Polymorphism. Joshua Dunfield and Neelakantan Krishnaswami International Conference on Functional Programming, 2013.