Ben Lippmeier

Graph based Type, Region, Effect, Closure, Mutability, Purity and Escape inference.
    - OR -
Drowning in Kinds.

"Pure programs are easier to reason about than programs with side effects" - thus speaks the folklore. Indeed, simple programs are easier to reason about than more complex ones - but what does this mean for production Haskell programs that are based totally around monad transformers and IORef?

Continuing on from our last talk, we show how the Hindley-Milner style type system used in Haskell can be extended to infer region, effect, and closure information - and more besides - without adversely affecting the programing model. We'll show that once we move to a graph based constraint solver, the extra support required for the region/effect/closure information is mostly orthogonal and straight forward to implement. We are also able to make use of existing support for type classes, and a mechanism similar to the coercion witnesses implemented in recent versions of GHC to help with GADTs.

We have a prototype compiler for a Haskell-like language which supports arbitrary side effects, including the destructive update of data structures, without needing Ref/IORef types. Our compiler uses region and effect annotations in the intermediate language to perform the same sort of code rewriting style optimizations present in GHC. We also support programmer introduced laziness and use the type system to ensure that only expressions without visible side effects may be suspended.