more on types
Remember: when we say \(e: t\), this means that as we evaluate \(e\), after all reductions we will get a thing of type \(t\).
type checking
- start at the leaves, integers and variables
- for each one above, match the expression to the type rules
a* type inference
- for every distinct lambda variable, we name a new type
- then, for function applications, we have then also substitute the output type of the function with a type variable
then, to saturating the constraint, we solve them using:
- \(t = a \implies a = t\)
- \(a = t_1, a = t_2 \implies a = t_1, a = t_2, t_1=t_2\)
- \(t_1 \to t_2 = t_3 \to t_4 \implies t_1 \to t_2 = t_3 \to t_4 = t_1 = t_3, t_2 =t_4\)
to then check and infer types
- we want to make sure no functions are int \(x \to y = int\)
- we want to make sure that an equation has no infinite solutions: \(int \to int \to \ldots\)
we do the first thing by staring at it real hard; we do the second thing by canonicalization.
canonicalization
- That no equation \(x \to y = int\) is present
- That the equations do not have infinite solutions
- Otherwise the program is ill-typed
we want every equivalent type to be represented by one thing.
- \(C(S, int) = int\)
- \(C(S, t\to t’) = C(S,t) \to C(S, t’)\)
- \(C(S, a) = C(S, t)\) if \(a = t \in S\), and \(t\) is not a type variable
- \(C(S, a) = C(S, b)\) if \(a = b \in S\), and \(a < b\) (for some oner)
- \(C(S, a) = a\), otherwise
This could go into an infinite loop—whenever you are canonicalizing something and you got the same expression twice you need to stop because you have an infinite loop. You can do this by keeping what you have seen of variables around.
let expression
god we finally have variables.
\begin{equation} let\ f = \lambda x.e\text{ in } e' \end{equation}
is equivalent to
\begin{equation} (\lambda f . e’) \lambda x .e \end{equation}
polymorphic types
universally quantified types
types are allowed to be what they were before
\begin{equation} t \to a | t \to t | int \end{equation}
but then we also have some kind of type qualifier
\begin{equation} o \to \forall a . o | t \end{equation}
key idea
“if we prove that \(e :t\), and the proof doesn’t rely on assumptions about \(\alpha\), then we have also proven \(e: \forall a. t\)”