Top

# Type Inference

## Type inference heuristically

Type inference by an experienced or clever person does not follow an algorithm, instead draws upon understanding, heuristics, experience, cleverness, shortcuts, and what mathematicians would call “obvious” and “by inspection”. Although not systematic, it can be faster and more insightful by skipping detailed bookkeeping and chores.

I do a few examples by heuristics first to motivate some non-obvious but important things needed in a type inference algorithm.

### Example 1 (creating unknowns)

Infer the type of `\x -> x`

I don't know what should be the type of x, but I can call it u, consider it unknown for now.

The code doesn't say anything about u, so the best I can do is:

`(\x -> x) :: u -> u`

What I do next depends on context:

• If I am asked to find the polymorphic type, e.g., because this is a standalone term, or because it is the RHS of a definition such as

`let f = \x -> x in ...`

then this `\x -> x` is really polymorphic, so I generalize to

`(\x -> x) :: ∀a. a -> a`

• If the larger term is like `(\x -> x) False`, then I discover the solution u = Bool, and conclude

`(\x -> x) False :: Bool`

In particular, I don't generalize, instead u stays as an unknown, and I hope that the context tells me what to do with it.

This doesn't look like an important point, but it can be very important in the big picture. By default, unless there is a reason for otherwise, treat u as an unknown that stands for only one type (monomorphic), even though we don't know what for now.

I will use names starting with u for unknowns, e.g., u1, u2, to serve as a reminder. When it is correct to generalize to a polymorphic type, I rename them to a, b, etc.

### Example 2 (solving for unknowns)

Assume 5::Integer, True::Bool

Infer the type of `\x y -> if False then (x, 5) else (True, y)`

`(x,5)::(u1,Integer)` with u1 unknown for x

`(True,y)::(Bool,u2)` with u2 unknown for y

if-then-else wants them to be the same type:

`(u1,Integer) = (Bool,u2)`

Solving that equation gives u1 = Bool, u2 = Integer.

Conclusion: `Bool -> Integer -> (Bool, Integer)`

### Example 3 (“type environment”)

`let b=False in \x y -> if b then (x, 5) else (True, y)`

If you're fast, it's just like the above.

If you go just a bit less fast, it goes like: I want to zoom into

`\x y -> if b then (x, 5) else (True, y)`

but with the knowledge b::Bool at the back of my mind, so that I can check that “`if b`” makes sense.

This indicates that an algorithm, or even an experienced person, keeps track of a “type environment” consisting of the variables in scope and their types for easy lookup.

Technically, I should also do that when working on lambdas, e.g., I now zoom into

`if b then (x, 5) else (True, y)`

and the type environment has b::Bool, x::u1, y::u2. But I was being fast.

### Example 4 (type mismatch error)

`\x -> if False then (x, 5) else (True, x)`

Similar thought process but the equation is

`(u1,Integer) = (Bool,u1)`

This means Integer = Bool. This is a type error, the “type mismatch” kind.

### Example 5 (“infinite type” error)

The other kind of type errors goes like this:

`\x -> if False then x else [x, x]`

I use unknown u1 for x. The equation to solve goes like

`u1 = [u1]`

Now, theoretically there is nothing wrong with that; the feature name is “infinite types”, and a few (very few) academic toy languages have been designed to support it.

But people find that it is rarely useful, it is hard to follow even when it is useful, and if a piece of practical code seems to do it, more than 99.9% of the time it's a typo rather than an intention, e.g., the author meant “`then [x]`”. So all practical languages and almost all academic languages ban it. (Statically typed languages, that is.)

In general, if an equation to solve goes like

u1 = ... something that mentions u1 ...

and is not simply “u1 = u1”, we say that it is a type error, and give the reason “infinite type”. You sometimes also see the wording “occurs check”; it means that the algorithm checks whether u occurs on the other side, and finds it.

In the rare case that you find an infinite type useful, the recommendation is to define an ordinary recursive wrapper type:

```data T = MkT [T]
-- so MkT :: [T] -> T

unT :: T -> [T]
unT (MkT list) = list
```

You now have to keep wrapping and unwrapping, but the logic is clearer because the code is explicit about when to think of one single T, when to think of a list of T's.

### Things needed by an algorithm

I need to create new names for new unknowns all the time.

I will run into equations like `(u1,Integer) = (Bool,u2)`, and I need to solve them and find out u1 = Bool, u2 = Integer. This solving is called “unification”; I was unifying `(u1,Integer)` with `(Bool,u2)`.

Because of that, I need a mutable table of solved unknowns. Every time I solve an equation, it causes an update. Since each entry is telling me to replace an unknown by its solution upon sight, this table is a table of substitutions.

I need the type inference algorithm to take one more parameter: a type environment to tell me which variables are in scope and what their types are. It is also a good place to hold the types of library functions.

## Unification algorithm

Unification solves two problems in one go: Checking whether two types match up, and if they contain unsolved unknowns, solve them, i.e., find out whether and what can be substituted for the unsolved unknowns to make the two types match up.

It doesn't return any value. It gives its answer in one of two ways: If the two types match up (perhaps after adding substitutions), return normally and update the table of substitutions; if not, abort with an error message.

### Substitutions

A mutable table of substitutions is maintained, initially empty. Every call to the unification algorithm can update the table. Notation for substitutions: “u := type”.

For clarity, I will make sure that solved unknowns don't appear in the RHS type, e.g., I won't let this table happen:

```u1 := [u2]     (won't happen, u2 is solved, change to u1 := [Integer])
u2 := Integer
```
Remark: Real implementations allow this and play clever, efficient tricks elsewhere. But I am going for least confusion for beginners.

Notation for applying all substitutions in the current table to rewrite a type: “apply-subst type”. This returns the rewritten type. I omit coding it up. Example: If the current table is

```u3 := Integer
u2 := u1->u1
```

then apply-subst `(u2, u4, Bool)` returns “`(u1->u1, u4, Bool)`”.

### Unification algorithm

The type inference algorithm is not always aware that an unknown is already solved and has an entry in the substitution table. It can call the unification algorithm with those unknowns in parameters. For clarity, I first use apply-subst on the parameters:

```unify T1 T2:
unify-intern (apply-subst T1) (apply-subst T2)
```

Remark: Real implementations don't need this, they play clever and efficient tricks elsewhere to compensate.

Then it is just a lot of simple cases:

```unify-intern u T
or
unify-intern T u
where u is an unknown:
if T=u:
return
else if u occurs in T:
infinite type error
else:
-- update table
add u:=T to the table
in the rest of the table, replace u by T, as promised
-- As explained, real implementations don't have to replace u by T

-- If T is also an unknown, e.g., unify-intern u2 u4,
-- should you add u2:=u4 or u4:=u2?
-- Answer: Doesn't matter, up to you.

unify-intern TC1 TC2
where TC1 and TC2 are type constants, e.g., Integer, Bool, Char:
if TC1 ≠ TC2:
type mismatch error
else
return

unify-intern [A] [B]
or
unify-intern (Maybe A) (Maybe B)
or similar cases:
unify-intern A B

unify-intern (S->T) (A->B)
or
unify-intern (S, T) (A, B)
or similar cases:
unify-intern S A
unify T B  -- Tricky! T or B may contain unknowns solved by unifying S and A.

unify-intern (S, T, U) (A, B, C):
similar, you get the idea

All other cases:
(e.g., unify-intern [u1] (Maybe u2))
type mismatch error
```

### Example

```                                               Current table:
u1 := u2 -> u3
unify u1 (u3->u4)
unify-intern (u2->u3) (u3->u4)
unify-intern u2 u3
add u3:=u2
replace u2 in the rest of the table
Updated table:
u1 := u2 -> u2
u3 := u2
unify u3 u4
unify-intern u2 u4
add u4:=u2
replace u4 in the rest of the table
Updated table:
u1 := u2 -> u2
u3 := u2
u4 := u2
```

## Type inference algorithm

Notation:

“infer env term”: Procedure call to infer the type of term; look up variables and types in env, the type environment. The answer is meant to be monomorphic, i.e., if there are unsolved unknowns, let them be, don't generalize to a polymorphic type.

“infer-poly env term”: call infer, then generalize to polymorphic type. (Example use case: To infer `let f = \x -> x in ...`, we will call infer-poly on `\x -> x`.)

If success, both return the type inferred; if failure, both throw an error.

Again, for least confusion for beginners, we also use apply-subst to all answers before returning them.

### Case: literal

```infer env True
return Bool

infer env 4
return Integer
-- For simplicity I don't cover type classes, I just nail 4 to Integer.

infer env []
create new unknown, say u
return [u]

Similarly for other literals.
```

### Case: variable

```infer env v
where v is a variable:
T := look up the type of v in env
(if not found, "var not found" error)
if T is polymorphic:
create new unknowns to instantiate with
T' := instantiate T
return (apply-subst T')
else
return (apply-subst T)
```

Example steps of needing instantiation:

```infer {x::u2, f::∀a b. a->b->a} f:
(∀a b. a->b->a  needs instantiation)
create unknowns u4, u5
return u4->u5->u4
```

### Case: lambda

```infer env (\v -> expr):
create new unknown (for v), say u
T := infer (env plus v::u) expr
return (apply-subst (u->T))
```

Remark: Although u starts as a new unknown, after the recursive call for expr, u may have been solved, so it may need a rewrite, even though T doesn't.

Example presentation of steps:

```infer {} (\x -> x):
create new unknown u1
T := infer {x::u1} x
return u1
T = u1
return u1->T = u1->u1
```

For lambdas of two or more parameters, you could treat as nested lambdas, `\x -> \y -> expr`, that's tedious. Let's shortcut it:

```infer env (\v w -> expr):
create new unknowns, say uv, uw
T := infer (env plus v::uv, w::uw) expr
return (apply-subst (uv->uw->T))
```

Example:

```infer {} (\x y -> x):
create new unknowns ux, uy
T := infer {x::ux, y::uy} x
return ux
T = ux
return ux->uy->ux
```

### Case: Function application

```infer env (f e):
Tf := infer env f
Te := infer env e
-- We now check Tf = Te->???, and find out what's ???
create new unknown u
unify Tf (Te -> u)
return (apply-subst u)
```

For multiple parameters, e.g., `f e1 e2`, again you can either treat as `(f e1) e2` or do the obvious shortcut.

Example steps:

```infer {} (\f x -> f (f x)):
create new unknowns u1, u2
T1 := infer {f::u1, x::u2} (f (f x)):
Tf := infer {f::u1, x::u2} f
return u1
Tf = u1

T2 := infer {f::u1, x::u2} (f x)
Tf2 := infer {f::u1, x::u2} f
return u1
Tf2 = u1
Tx := infer {f::u1, x::u2} x
return u2
Tx = u2
create new unknown u3
unify Tf2 (Tx -> u3)
unify-intern u1 (u2 -> u3)
Updated table:
u1 := u2 -> u3
return u3
T2 = u3

create new unknown u4
unify Tf (T2 -> u4)
unify-intern (u2 -> u3) (u3 -> u4)
Updated table:
u1 := u2 -> u2
u3 := u2
u4 := u2

return (apply-subst u4) = u2
T1 = u2
return (apply-subst (u1->u2->T1)) = (u2->u2)->u2->u2
```

### Case: let (single definition, non-recursive)

People expect these to be legal:

```let f = \x -> x    -- expect f :: ∀a. a -> a
in (f True, f 4)

let e = []            -- expect e :: ∀a. [a]
in (True : e, 4 : e)
```

This means when “let” is used for local definitions (and similarly for “where”), we need to generalize an inferred type to a polymorphic type, e.g., `\x -> x` is normally just `u -> u` where `u` is an unknown, but here it is generalized to ```∀a. a -> a``` so `f` is polymorphic.

```infer env (let v = exprv in expr)
Tv := infer-poly env exprv
infer (env plus v::Tv) expr

infer-poly env expr:
T := infer env expr
for each unknown ui in T:
if ui doesn't also appear in env:
create new type variable, say ai
return (∀(the ai's) . (T but replace each ui by ai))
-- Example: T = u2 -> u3 -> u4
-- u3 appears in env, u2 and u4 don't
-- return (∀a2 a4. a2 -> u3 -> a4)
```

Example:

```infer {} (let f = \x -> x in (f True, f 4))
T := infer-poly {} (\x -> x)
S := infer {} (\x -> x)
...
return (u1 -> u1)
S = u1 -> u1
return ∀a. a -> a
T = ∀a. a -> a
infer {f :: ∀a. a -> a} (f True, f 4)
-- I haven't written the rule for tuples, but you can extrapolate from
-- the section on algebraic data types below, and it would go like this:

T1 := infer {f :: ∀a. a -> a} (f True)
Tf := infer {f :: ∀a. a -> a} f
(∀a. a -> a  needs instantiation)
create new unknown u2
return (u2 -> u2)
Tf = (u2 -> u2)
Te := infer {f :: ∀a. a -> a} True
return Bool
Te = Bool
create new unknown u3
unify Tf (Te -> u3)
unify-intern (u2 -> u2) (Bool -> u3)
Updated table:
u2 := Bool
u3 := Bool
return (apply-subst u3) = Bool
T1 = Bool

T2 := infer {f :: ∀a. a -> a} (f 4)
Tf := infer {f :: ∀a. a -> a} f
create new unknown u4
return (u4 -> u4)
Tf = (u4 -> u4)
Te := infer {f :: ∀a. a -> a} 4
return Integer
Te = Integer
create new unknown u5
unify Tf (Te -> u5)
unify-intern (u4 -> u4) (Integer -> u5)
Updated table:
u2 := Bool
u3 := Bool
u4 := Integer
u5 := Integer
return (apply-subst u5) = Integer
T2 = Integer
return (T1, T2) = (Bool, Integer)
```

The following example explains why we don't generalize an unknown that appears in the type environment: We expect these:

```(\x -> let y = x in not y) :: Bool -> Bool
(\x -> let y = x in (not y, take 1 y))  -- type mismatch error
```

Explanation: A lambda gives the parameter x one single type, so if y=x then y also takes that single type.

```infer {not::Bool->Bool} (\x -> let y = x in not y)
create new unknown ux
T := infer {not::Bool->Bool, x::ux} (let y = x in not y)
Ty := infer-poly {not::Bool->Bool, x::ux} x
Tx := infer {not::Bool->Bool, x::ux} x
return ux
Tx = ux
-- ux not generalized
return ux
Ty = ux
infer {not::Bool->Bool, x::ux, y::Ty=ux} (not y)
... some steps that results in ...
Updated table:
ux := Bool
and a few others
return Bool
T = Bool
return apply-subst (ux -> T) = Bool -> Bool
```

### Case: if-then-else

```infer env (if cond then e1 else e2):
-- check cond :: Bool
Tcond := infer env cond
unify Tcond Bool

-- find types of e1, e2
Te1 := infer env e1
Te2 := infer env e2

-- but they have to be the same!
unify Te1 Te2
return (apply-subst Te1)
```

### Algebraic data types (unparameterized)

An algebraic data type definition gives you data constructors so you can make terms of that type, and pattern matching so you can use terms of that type. Accordingly, it adds a group of type inference rules for making, and a type inference rule for pattern matching.

I will illustrate by an example type. Then you extrapolate to other types.

```data MI = Non | Has Integer
```

Making: Add these rules:

```infer env Non
return MI

infer env (Has expr):
T := infer env expr
unify T Integer
return MI
```

Do you have to add those rules? Not really, but if you are hand-executing type inference on examples, it is faster to add and use them.

If you are coding up a type inference algorithm, then it is less coding to: Allow type environments to also have data constructors, e.g., include these:

```Non :: MI
Has :: Integer -> MI
```

and recall that `Has expr` can be treated as function application. This is easier to code up, but more tedious and less insightful to execute by hand.

Using, pattern matching: For simplicity I just cover case-expressions with simple patterns:

```case eMI of { Non -> e0 ; Has x -> e1 }
```

We definitely need to add a custom rule for pattern matching against the data constructors.

```infer env (case eMI of { Non -> e0 ; Has x -> e1 }):
-- check eMI :: MI
T := infer env eMI
unify T MI

-- infer e0
T0 := infer env e0

-- infer e1, note that local var x::Integer is in scope
T1 := infer (env plus x::Integer) e1

-- but they have to be the same!
unify T0 T1
return (apply-subst T0)
```

### Algebraic data types (parameterized)

Parameterized algebraic data types are similar, but there are additional unknowns to create for instantiating the polymorphic types. Example:

```data Maybe a = Nothing | Just a
```

The data constructors are polymorphic:

```Nothing :: ∀a. Maybe a
Just :: ∀a. a -> Maybe a
```

Making:

```infer env Nothing
create new unknown u
return (Maybe u)

infer env (Just expr)
T := infer expr
return (Maybe T)
```

Two ways to explain why `Just expr` is that simple:

• If `expr :: T`, then `Just expr :: Maybe T`, “obviously”. :)

• If you do it the careful way:

```  -- Just :: ∀a. a -> Maybe a
-- so create an unknown u to instantiate it,
-- so Just :: u -> Maybe u in this context
create new unknown u

-- but "Just expr", with expr :: T, needs T = u
unify T u

-- then Just expr :: Maybe u
return (apply-subst (Maybe u))
```

That's always `Maybe T`.

Using, pattern matching:

```infer env (case eM of { Nothing -> e0; Just x -> e1 }):
-- check eM :: Maybe ???
T := infer env eM
create new unknown u
unify T (Maybe u)

-- infer e0
T0 := infer env e1

-- infer e1, note local var x::u since eM = Just x :: Maybe u
T1 := infer (env plus x::u) e1

-- but they have to be the same!
unify T0 T1
return (apply-subst T0)
```

Extrapolate this to standard parameterized types such as lists and tuples.

The 2-tuple type can be understood as

```data Tuple2 a b = MkTuple2 a b
```

except for the syntactic change from `MkTuple e1 e2 :: Tuple2 T1 T2` to `(e1, e2) :: (T1, T2)`

The list type can be understood as

```data List a = Nil | Cons a (List a)
```

except for the syntactical change from `[]` to `Nil`, `Cons e1 e2` to `e1 : e2`.

### Not covered this time

Multiple definitions and recursive definitions. Programmer-provided type signatures. Type classes.