So I’ve been here at MSR Cambridge for almost two weeks now (!), working in the Programming Principles and Tools Group with Simon Peyton-Jones and Dimitrios Vytiniotis — and also collaborating with Stephanie Weirich and Steve Zdancewic, who are also in Cambridge. So, what have I been doing?

This week, Simon, Dimitris, and I have been having a major GHC hacking session, implementing the new constraint-solving type inference engine described in their new OutsideIn(X) paper. It’s been a lot of fun — I’ve never hacked on GHC before, and it’s quite a new experience hacking on such a large (and amazing) piece of software. I’ve been working on the *constraint canonicaliser*, which puts constraints into canonical forms appropriate for the constraint simplifier to work with. As a simple example, the equality constraint `(Int, a) ~ (b, Char)`

gets decomposed into the primitive constraints `Int ~ b`

and `a ~ Char`

. It’s also responsible for flipping and flattening equality constraints so that type function applications only happen on the left-hand side: for example, the constraint `F a b ~ G Int`

(where both `F`

and `G`

are type families), gets rewritten to a pair of constraints `F a b ~ c`

, `G Int ~ c`

, where `c`

is a fresh variable. If we didn’t do this it would lead to problems with termination: for example, the constraint `a ~ [F a]`

could lead to infinite rewriting of `a`

to `[F a]`

to `[F [F a]]`

to… (And before you protest that we ought to just throw out `a ~ [F a]`

on the grounds that it is recursive, note that `F a`

may not mention `a`

at all; for example, perhaps `F`

is defined by `F [x] = Int`

.)

Constraints also include type class constraints and implicit parameter constraints, although there’s much less work to do with those as far as canonicalisation is concerned.

Next week, I’ll likely get back to our other, more ambitious research project, but I’ll write more about that next time. In the meantime, if you’re in or near Cambridge and want to meet up, just drop me a note!

As a simple example, the equality constraint (Int, a) ~ (b, Char) gets decomposed into the primitive constraints Int ~ b and a ~ Char.Is not this called a unification instead of canonicalisation (e.g. Robinson’s algorithm)?

Unification is essentially a method for solving simple equality constraints. However, GHC has to solve other sorts of constraints (type class constraints, implicit parameter constraints) as well, and even the equality constraints are made more complicated by the presence of type functions — for example, if F is a type function then the fact that F a ~ F b does not imply a ~ b.

Actually it is not clear to me how “type class constraints” and “implicit parameter constraints” differ from “equality constraints” — these notions may intersect or not intersect. Your “~” seems to be simply “=”. BTW is your work somehow related to Coq’s type inference mechanism?

F is a type function then the fact that F a ~ F b does not imply a ~ b.It is about injectivity of F.

Yes, ~ is just the notation used in GHC for type equality. I’m not sure of the relationship to Coq’s type inference.

Type class constraints are quite different from equality constraints, I’m not sure what you mean by saying the notions may or may not intersect. For example if we have a constraint (Monoid m) it means that m is constrained to be a type which has a Monoid instance; it has nothing to do with equality.

About injectivity of type functions, yes, that’s exactly right: usually normal type constructors (e.g. Maybe) are injective, so if we encounter Maybe a ~ Maybe b during unification we know a ~ b. But with non-injective type functions, when we encounter F a ~ F b we can’t (yet) conclude anything more about a and b — but we must still remember the fact that F a ~ F b in some suitable form, because we may need it later. So standard unification (which keeps track of a substitution from type *variables* to types) is not appropriate.

Yes, I made a mistake, I completely forgot that. Your simple example is suitable for unification so I was misled.