Simple Uni cation-based Type Inference for GADTs
Simon Peyton Jones
Microsoft Research, Cambridge
Dimitrios Vytiniotis Stephanie Weirich
Geoffrey Washburn
University of Pennsylvania
Abstract
Generalized algebraic data types (GADTs), sometimes known as
guarded recursive data types or rst-class phantom type s , are a
simple but powerful generalization of the data types of Haskell and
ML. Recent works have given compelling examples of the utility
of GADTs, although type inference is known to be dif cult. Our
contribution is to show how to exploit programmer-supplied type
annotations to make the type inference task almost embarrassingly
easy. Our main technical innovation is wobbly types, which express
in a declarative way the uncertainty caused by the incremental
nature of typical type-inference algorithms.
Categories and Subject Descriptors D.3.3 [PROGRAMMING
LANGUAGES]: Language Constructs and Features abstract data
types, polymorphism
General Terms Languages, Theory
Keywords generalized algebraic data types, type inference
1. Introduction
Generalized algebraic data types (GADTs) are a simple but potent
generalization of the recursive data types that play a central role
in ML and Haskell. In recent years they have appeared in the
programming language literature with a variety of names (guarded
recursive data types [25], rst-class phantom types [5], eq uality-
quali ed types [18], and so on), although they have a much lon ger
history in the dependent types community. Any feature with so
many names must be useful and indeed these papers and others
give many compelling examples.
It is time to turn GADTs from a specialized hobby into a main-
stream programming technique, by incorporating them as a con-
servative extension of Haskell (a similar design would work for
ML). The main challenge is integrating GADTs with type inference,
a dominant feature of Haskell and ML.
Rather than seeking a super-sophisticated inference algorithm,
an increasingly popular approach is to guide type inference using
programmer-supplied type annotations. With this in mind, our cen-
tral focus is this: we seek a declarative type system for a language
that includes both GADTs and programmer-supplied type annota-
tions, which has the property that type inference is straightforward.
Our goal is a type system that is predictable enough to be used by
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for pro t or commercial advantage and that copies bear this n otice and the full citation
on the rst page. To copy otherwise, to republish, to post on s ervers or to redistribute
to lists, requires prior speci c permission and/or a fee.
ICFP’06 September 16 21, 2006, Portland, Oregon, USA.
Copyright c© 2006 ACM 1-59593-309-3/06/0009. . . $5.00.
ordinary programmers; and simple enough to be implemented with-
out heroic efforts. We make the following speci c contribut ions:
• We specify a programming language that supports GADTs and
programmer-supplied type annotations (Section 4). The key in-
novation in the type system is the notion of a wobbly type (Sec-
tion 3), which models the places where an inference algorithm
would guess . The idea is that type re nements induced by
GADTs never re ne wobbly types, and hence type inference is
insensitive to the order in which the algorithm traverses the ab-
stract syntax tree.
• Like any system making heavy use of type annotations, we offer
support for lexically scoped type variables that can be bound
by both polymorphic type signatures and signatures on patterns
(Section 4.5 and 5.5). There is no rocket science here, but we
think our design is particularly simple and easy to specify,
certainly compared to our earlier efforts.
• We explore a number of extensions to the basic system, includ-
ing improved type checking rules for patterns and case expres-
sion scrutinees, and nested patterns (Section 5).
• We prove that our type system is sound, and that it is a con-
servative extension of a standard Hindley-Milner type system
(Section 6). Moreover our language can express all programs
that an explicitly-typed language could express.
• We sketch a type inference algorithm for our type system that is
a modest variant of the standard algorithm for Hindley-Milner
type inference. We prove that this algorithm is sound and com-
plete (Section 6.3).
Space restrictions prohibit a complete presentation of these con-
tributions. The details of the algorithm and related technical mate-
rial are given in a companion technical report [23]1.
We have implemented type inference for GADTs, using wobbly
types, in the Glasgow Haskell Compiler (GHC). GHC’s type checker
is already very large; not only does it support Haskell’s type classes,
but also numerous extensions, such as functional dependencies,
implicit parameters, arbitrary-rank types, and more besides. An
extension that required all this to be re-engineered would be a non-
starter, and it is here that the simplicity of our GADT inference
algorithm pays off. In particular, we have successfully extended
GHC to support both GADTs and impredicative polymorphism
(described in a companion paper in this volume [22]), without
undesirable interactions with each other, or with existing features.
Our implementation has already received heavy use. The re-
leased implementation in GHC uses a more complicated scheme
than that described here, originally given in an earlier version of
this paper (see Section 7). We are in the midst of re-engineering the
implementation to match what we describe in this revised, simpler
version.
1 www.cis.upenn.edu/~dimitriv/dimitriv-inference.html
ICFP’06 1 2006/12/19

2. Background
By way of background, we use a standard example to remind the
reader of the usefulness of GADTs. Here is a declaration of a Term
data type for a simply-typed language:
data Term a where
Lit :: Int -> Term Int
Inc :: Term Int -> Term Int
IsZ :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
Pair :: Term a -> Term b -> Term (a,b)
Fst :: Term (a,b) -> Term a
Snd :: Term (a,b) -> Term b
Term has a type parameter a that indicates the type of the term it
represents, and the declaration enumerates the constructors, giving
each an explicit type signature. We note that the type parameter a is
a dummy parameter used only to indicate the kind of Term, and
does not scope over the types of the constructors. All type variables
in the types of constructors are implicitly universally quanti ed.
We adopt this convention for the examples appearing in the rest of
this paper. Equivalently one could write
data Term :: * -> * where ...
The type signatures of the constructors only allow
one to construct well-typed terms; for example, the term
(Inc (IsZ (Lit 0))) is rejected as ill-typed, because
(IsZ (Lit 0)) has type Term Bool and that is incompatible
with the argument type of Inc.
An evaluator for terms is stunningly direct:
eval :: Term a -> a
eval (Lit i) = i
eval (Inc t) = eval t + 1
eval (IsZ t) = eval t == 0
eval (If b t e) = if eval b then eval t else eval e
eval (Pair a b) = (eval a, eval b)
eval (Fst t) = fst (eval t)
eval (Snd t) = snd (eval t)
It is worth studying this de nition. Note that the right hand
side of the rst equation patently has type Int, not a. But, if
the argument to eval is a Lit, then the type parameter a must
be Int (because the Lit constructor only produces terms of type
Term Int), and so the right hand side has type a also. Similarly,
the right hand side of the third equation has type Bool, but in a
context in which a must be Bool. And so on.
The key ideas of the semantics for GADTs are these:
• A generalized data type is declared by enumerating its construc-
tors, giving an explicit type signature for each. In conventional
data types in Haskell or ML, the result type of a data construc-
tor must be the type constructor applied to all of the type pa-
rameters of the data constructor. In a generalized data type, the
result type must still be an application of the type constructor,
but the argument types are arbitrary. For example Lit mentions
no type variables, Pair has a result type with structure (a,b),
and Fst mentions some, but not all, of its universally-quanti ed
type variables.
• The data constructors are functions with ordinary polymorphic
types. There is nothing special about how they are used to
construct terms, apart from their unusual types.
• All the excitement lies in pattern matching. Matching against a
constructor may induce a type re nement in the case alternative.
For example, in the Lit branch of eval, we can re ne a to Int.
• The dynamic semantics is unchanged. Pattern-matching is done
on data constructors only and there is no run-time type passing.
The eval function is a somewhat specialized example, but earlier
papers have given many other applications of GADTs, including
generic programming, modeling programming languages, main-
taining invariants in data structures (e.g. red-black trees), express-
ing constraints in domain-speci c embedded languages (e.g . secu-
rity constraints), and modeling objects [8, 25, 5, 18, 16, 17]. The
interested reader should consult these works; meanwhile, for this
paper we simply take it for granted that GADTs are useful.
3. The key idea
Our goal is to combine the exibility of Hindley-Milner type infer-
ence with the expressiveness of GADTs, by using the programmer’s
annotations to guide type inference. Furthermore, we seek a system
that gives as much freedom as possible to the inference algorithm.
For example, we would like to retro- t GADT inference to existing
compilers, as well as use it in new ones.
The dif culty with type inference for GADTs is well illustrated
by the eval example of Section 2. In the absence of the type
signature for eval, a type inference engine would have to anti-
re ne the Int result type for the rst two equations, and the Bool
result type of the third (etc.), to guess that the overall result should
be of type a. Such a system would certainly lack principal types.
Furthermore, polymorphic recursion is required: for example, the
recursive call to eval in the second equation is at type Int, not a.
All of these problems go away when the programmer supplies the
type of eval.
Furthermore, the complete type of a function that uses GADTs
is required, because, even if the return type is clear, type inference
may still be challenging. Here is another variant:
f x y = case x of
Lit i -> i + y
other -> 0
There are at least two types one could attribute to f, namely
Term a→ Int→ Int and Term a→ a→ Int. The latter works
because type re nement induced by the pattern match on x re nes
the type of y. Alas, neither is more general than the other. Again, a
programmer-supplied type signature would solve the problem.
Thus motivated, our main idea is the following:
Type re nement applies only to user-speci ed types.
In the case of f, since there are no type annotations, no type
re nement will take place: x must have type Term Int and y will
get type Int. However, if the programmer adds a type annotation,
the situation is quite different:
f :: Term a -> a -> Int
f x y = case x of
Lit i -> i + y
other -> 0
Now it is obvious that x has type Term a and y has type a. Be-
cause the scrutinee of the case has the user-speci ed type Term a,
the case expression does type re nement, and in the branch the
type system knows that a = Int. Because the type of y is also
user-speci ed, this type re nement is applied when y occurs in the
right hand side.
To summarise, our general approach is this:
• Instead of user-speci ed type , we use the briefer term rigid
type to describe a type that is completely speci ed, in some
direct fashion, by a programmer-supplied type annotation.
• A wobbly type is one that is not rigid. There is no such thing as
a partly-rigid type; if a type is not rigid, it is wobbly2 .
• A variable is assigned a rigid type if it is clear, at its binding
site, precisely what its type should be.
2
In an earlier version of this paper, types were allowed to have both rigid
and wobbly components (Section 7).
ICFP’06 2 2006/12/19