The case for compositional type checking

23 October 2010 (programming haskell language ELTE) (1 comment)

This is an based on a chapter of the M.Sc. thesis I am writing at ELTE, supervised by Péter Diviánszky.

For my M.Sc. thesis, I've been working on writing a compositional type checker for Haskell 98. The basic idea is to extend Olaf Chitil's compositional type system with ad-hoc polymorphism, Haskell 98's major extension to the Hindley-Milner type system. In this post, I'm showing the motivation behind wanting to go compositional.

A property shared by both commonly-used algorithms for doing Hindley-Milner type inference, W and M, is that both W and M infer the type of composite expressions by inferring one subexpression (in some sense, the “first” one) and using its results in inferring the type of the “next” one. They are linear in the sense that partial results are threaded throughout the type inference.

The effect of linearity on type inference is that certain sub-expressions (those that are processed earlier) can have greater influence on the typing of other subexpressions. This is bad because it imposes a hierarchy on the subexpressions that is determined solely by the actual type checking algorithm, not by the type system; thus, it can lead to misleading error messages for the programmer.

For example, let's take the following definition of a Haskell function:

foo x = (toUpper x, not x)

There are two ways to typecheck this definition using W: either we first typecheck toUpper x, using the context {x :: α}, resulting in the type equation α ~ Char, then checking not x with {x :: Char}, or do it the other way around, by first looking at not x, then as a result recursing into toUpper x with the context {x :: Bool}.

GHC, it seems, does the former, resulting in the following error message:

Couldn't match expected type `Bool' against inferred type `Char'
In the first argument of `not', namely `x'
In the expression: not x
In the expression: (toUpper x, not x)

Whereas Hugs 98 does the latter:

ERROR "test.hs":1 - Type error in application
*** Expression : toUpper x
*** Term : x
*** Type : Bool
*** Does not match : Char

The problem is that they are both misleading, because there is nothing wrong with either not x or toUpper x by itself. The problem only comes from trying to unify their respective views on the type of x.

A compositional type checker, in contrast, descends into toUpper x and not x using the same context, {x :: α}. The first one results in the typing (which is defined to be not just the type of an expression, but also a mapping of monomorphic variables to their types) {x :: Char} ⊢ Char, and the second one in {x :: Bool} ⊢ Bool. Only afterwards are these two typings tried to be unified.

This is better because it becomes meaningful to talk about the typing of a subexpression. For the example above, my work-in-progress compositional type checker can report errors with an (IMO) much more helpful message:

(toUpper x, not x)
Cannot unify `Char' with `Bool' when unifying `x':
      toUpper x    not x
      Char         Bool
x ::  Char         Bool

Of course, the devil's in the details — but that's what my thesis will be about.

« Pom-pom poporopo-pom 
All posts
 Logicomix »

Cale Gibbard 2010-10-26 14:09:57

Interesting idea! It's probably a lot more work again to integrate this sort of approach into GHC's fancy type system, but the improvement it would make to some error messages would be quite valuable.

One nitpick: please don't refer to typeclass polymorphism as ad-hoc. :) The original paper by Wadler and Blott on typeclasses referred to them as a sort of approach to ad-hoc polymorphism, but the distinction has become clearer over time. It has more in common with parametric polymorphism than it does with ad-hoc polymorphism. In particular, new typeclass-polymorphic values can be constructed simply by using existing ones, rather than making separate definitions at each type required.

While it's possible to simulate ad-hoc polymorphism using typeclasses having only one method with an arbitrary type, this is rarely how they're actually used.