<![CDATA[
# Type Inference
Today we will practice using the HM type inference algorithm and the unification algorithm.
##### Exercise: infer [✭✭]
Using the HM type inference algorithm, infer the type
of the following definition:
```
let apply f x = f x
```
Remember to go through these steps:
* desugar the definition entirely (i.e., construct an AST)
* assign preliminary type variables (i.e., annotate the AST)
* collect constraints
* solve the constraints
For solving the constraints, go ahead and solve by hand rather than
using the unification algorithm in the notes.
When you're done solving, you will be left with some preliminary
type variables that have no concrete types (e.g., `int`) associated
with them. Those can be renamed to OCaml type variables
such as `'a` and `'b`.
If you get stuck, consult the [lecture notes](notes.html).
□
##### Exercise: infer s [✭✭]
Using the HM type inference algorithm, infer the type
of the following definition:
```
let s x y z = (x z) (y z)
```
□
##### Exercise: infer if [✭✭]
In lecture we gave the constraint collection rules for several
but not all of OCaml's expression forms. How should constraints
be collected from an expression of the form `if e1 then e2 else e3`?
Your answer should be a completion of the following:
```
U(e1) = ...
U(e2) = ...
U(e3) = ...
and all constraints collected from e1, e2, and e3
```
*Hint: recall the type checking rule for if expressions.*
Using your answer, infer the type of this expression:
```
if true then 3110 else 0
```
□
##### Exercise: unify [✭✭]
Use the unification algorithm in the [lecture notes](notes.html)
to solve the following system of constraints. Your answer should
be a *substitution*, in the sense that the unification algorithm
defines that term.
```
X = int
Y = X -> X
```
□
## Additional exercises
##### Exercise: infer double [✭✭]
Using the HM type inference algorithm, infer the type
of the following definition:
```
let double f x = f (f x)
```
□
To infer the type of a match expression, we need to collect
constraints from patterns. A variable pattern is a defining
occurrence of a variable, so there aren't any constraints
to collect from the pattern. For example, in this pattern:
```
match e with
| x -> e'
```
the variable `x` is defined by the pattern and could be used
in expression `e'`.
Other forms of patterns do generate constraints. For example:
```
U(n) = int (where n is an integer constant pattern)
U(s) = string (where s is a string constant pattern)
U((p1,p2)) = U(p1) * U(p2)
```
##### Exercise: infer match [✭✭✭]
How should constraints be collected from an expression of the
form `match e with p1 -> e1 | ... | pn -> en`?
Your answer should be a completion of the following:
```
U(ei) = ...
U(pi) = ...
and all constraints collected from e, and all pi, ei
```
*Hint: recall the type checking rule for match expressions.*
Using your answer, infer the type of this expression:
```
match 3110 with x -> x+1
```
□
##### Exercise: unify more [✭✭✭]
Use the unification algorithm in the [lecture notes](notes.html)
to solve the following system of constraints. Your answer should
be a *substitution*, in the sense that the unification algorithm
defines that term.
```
X -> Y = Y -> Z
Z = U -> W
```
□
]]>