[Haskell-cafe] Modular type inference

[Simon Peyton-Jones]

Friends

Many of you will know that I've been muttering about re-engineering GHC's type inference engine for some time now.  Dimitrios, Tom, Martin and I have just completed an epic paper describing the Glorious New Framework that forms the substance of the above mutterings:
	http://haskell.org/haskellwiki/Simonpj/Talk:OutsideIn

We'd love comments and feedback. Dimitrios and I plan to roll up our sleeves and implement it in June.

Simon

Modular type inference with local assumptions: OutsideIn(X)

Abstract. Advanced type system features, such as GADTs, type classes, and type families have have proven to be invaluable language extensions for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference, because they introduce local type assumptions.

In this article we present a novel constraint-based type inference approach for local type assumptions. Our system, called OutsideIn(X), is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm.

Going beyond the general framework, we also give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right.