Type Inference for Expressive Types

Type inference is and will always be one of the topics I am most interested in. Expressive types demand a significant departure from standard Hindley/Milner inference where we are only concerned with solving sets of primitive constraints such as type equations and type classes. In case of expressive types, the typing problem is captured in terms of solutions of the richer form of implication constraints. I co-designed a system [11] which precisely points out this connection. There are a number of other important results such as the first formal investigation why type inference for GADTs is such as hard problem and a novel inference method based on Herbrand abduction [1]. Further results include the first formal proof that type inference under the GHC multi-parameter type class conditions yields principal types [8]. Some of these results can also be found in earlier works [24,25,28].

Martin Sulzmann 2006-07-19