## 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)

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

*** 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:

`input/test.hs:1:8-25:`

(toUpper x, not x)

Cannot unify `Char' with `Bool' when unifying `x':

toUpper x not x

Char Bool

x :: Char Bool

(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.

## 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.