You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Future self - I'm leaving this as-is because it was quite a climb, but in the end I didn't take the approach
described here. The trouble was that tying to implement Algorithm W as described below, using substitutions,
resulted in a horrible unmaintainable mess of code which I confess I didn't even understand myself. I discovered
a little secret about HM though, There is an alternative much more pragmatic approach, much closer to
the actual implementations I've seen, and described originally in this paper
which uses prolog-style logical variables with pruning, proper type-environments, and a reference implementation
in Modula-2. Ripping out the old type-checker and adding in the new on only took me a couple of weeks over Christmas,
wheras I must have spent two months or more on the previous version, which never even worked properly.
Or, "Climbing the Hindley-Milner Mountain" 😁
My notes on an absolutely fantastic YouTube series by Adam Jones.
These are initially for my own benefit, explaining it to myself, so if you don't follow go watch the videos.
You might think that the $\mathtt{[let]}$ term is redundant, because $\mathtt{let\ x = e_1\ in\ e_2}$
is synonymous with $(\lambda x.e_2)e_1$ but $\mathtt{let}$ is treated differently by the type-checking
algorithm, as a way to achieve polymorphism.
Free Variables in Expressions
Free variables are variables that have no value (free as in "not bound").
We can define a free variables function
$\mathcal{FV}$ for lambda expressions as
$\tau$ is a monotype, which can be a siple type $\alpha$ like int or string, or
it can be a "type function application" $C$ like $\mathtt{List[}\tau\mathtt{]}$ or $\tau_1 \rightarrow \tau_2$.
$\mathtt{Bool}$, $\mathtt{Int}$ etc are also type function applications, but with no arguments.
$\sigma$ is a polytype
which can be either a monotype $\tau$ or a quantified polytype $\forall\alpha.\sigma$. Quantified polytypes
are how we deal with polymorphic functions. More on that lter, but essentially $\forall\alpha$ is saying
"any $\alpha$ in the subsequent expression is local to it".
These two types are not interchangeable. pay careful attention to where we use a $\tau$ and where we use a $\sigma$
in subsequent equations.
The interesting thing here is the quantifier rule which starts to hint at how polymorphism is handled: $\alpha$ is not free in
a polytype quantified by $\alpha$.
Free Variables in Contexts
We can also describe a rule for free variables in a context, referring back to the Context Grammar above,
Substitutions are sets of mappings from symbols to terms, where terms are general constructions of symbols,
like arithmetic expressions etc. Mappings are applied simultaneously.
says $S$ is the substitution mapping $\mathtt{h}$ to $\mathtt{l}$ etc.
so if $\mathtt{h}$ etc. are characters, then
$$
S(\mathtt{hello}) = \mathtt{lasso}
$$
Note that $\mathtt{h}$ in $\mathtt{hello}$ went to $\mathtt{l}$, but was not subsequently mapped to $\mathtt{s}$.
That is what the "mappings are applied simultaneously" rule was about.
Substitutions in Type Systems
Direct quote:
Hindley-Milner type inference algorithms use substitutions from type variables to monotypes,
applied on types.
$S_3$ is different, so the order of application matters.
A semi-manual way to calculate the composition of two substitutions like this is
to draw up a table. The leftmost column is the symbols being mapped from,
intermediate columns are the results of applying a substitution on the previous
column, and the final column is the resulting mapping:
$S_2$
$S_1$
$S_3$
$\mathtt{h}$
$\mathtt{i}$
$\mathtt{i}$
$\mathtt{h} \mapsto \mathtt{i}$
$\mathtt{o}$
$\mathtt{h}$
$\mathtt{i}$
$\mathtt{o} \mapsto \mathtt{i}$
The set of the mappings in column $S_3$ is the final substitution:
$\set{\mathtt{h} \mapsto \mathtt{i}, \mathtt{o} \mapsto \mathtt{i}}$
Unifying Substitutions
Another direct quote:
A substitution unifies two values if, when applid to both, the results are equal.
We can also ask "what substitution unifies $a$ and $b$?" There are obviously many possible
substitutions in this case.
The substitution with the fewest mappings is called the "Most General Unifying Solution".
If we rely on the fact that substitutions always map from symbols, this sometimes restricts the possible solutions,
for example
$$
\begin{align}
a &= 3 + (7 \times z)
\\
b &= y + (x \times 2)
\\
S &= \set{ y \mapsto 3, x \mapsto 7, z \mapsto 2 }
\end{align}
$$
another example
$$
\begin{align}
a &= 2 + 3
\\
b &= y
\\
S &= \set { y \mapsto 2 + 3 }
\end{align}
$$
Just demonstrates that the expressions in a substitution can be complex.
Another example
$$
\begin{align}
a &= 3 \times 7
\\
b &= 3 + z
\end{align}
$$
In this case there is no unifying solution.
Another example
$$
\begin{align}
a &= 1 + z
\\
b &= z
\\
S &= \set{ z \mapsto 1 + 1 + 1 + \dots }
\end{align}
$$
This is a solution, but it's not ok, attempting to unify a variable with an
expression that it occurs in results in an infinite expansion which might be
ok mathematically, but it's no use to a type checking algorithm.
Anyway this all gives us a signature for the unification functon which I'm calling $\mathcal{U}$:
$$
\begin{align}
S &= \mathcal{U}(a, b)
\\
S(a) &= S(b)
\end{align}
$$
Applying Unification to Type Systems
Example
$$
\begin{align}
a &= \mathtt{Int} \rightarrow \alpha
\\
b &= \beta \rightarrow \mathtt{Bool}
\\
S &= \mathcal{U}(a, b)
\\
S &= \set{ \alpha \mapsto \mathtt{Bool}, \beta \mapsto \mathtt{Int} }
\end{align}
$$
Another example
$$
\begin{align}
a &= \mathtt{List}\ \alpha
\\
b &= \beta \rightarrow \mathtt{Bool}
\\
S &= \mathcal{U}(a, b)
\end{align}
$$
Has no solutions as the structure is different.
Another example
$$
\begin{align}
a &= \alpha \rightarrow \mathtt{Int}
\\
b &= \alpha
\\
S &= \mathcal{U}(a, b)
\\
S &= \set{\alpha \mapsto \mathtt{Int} \rightarrow \mathtt{Int} \rightarrow \mathtt{Int} \rightarrow \dots}
\end{align}
$$
This is the "occurs in" error again, $\alpha$ is a function with an infinite number of arguments.
Unification Algorithm for HM Types
unify(a: Monotype, b: Monotype) -> Substitution:
if a is a type variable:
if b is the same type variable:
return {}
if b contains a:
throw "Error occurs check"
return { a -> b }
if b is a type variable:
return unify(b, a)
if a and b are both type function applications:
if a and b have different type functions:
throw "Error unification failed"
S = {}
for i in range(number of type function arguments):
S = combine(S, unify(a.args[i], b.args[i])
return S
Just remember that we're talking about type function applications here, not lambdas, i.e. if the type
function application is $\mathtt{List}\ \beta$ then the arguments are $\beta$, or if the type
function application is $\mathtt{Int}\rightarrow\alpha$ then the arguments are $\mathtt{Int}$ and $\alpha$,
and if the type function application is $\mathtt{Int}$ then there are no arguments.
and in fact $\forall\alpha.\alpha$ is like zero in this relation, it's the most general possible type expression
because it means any type variable.
Formal Definition of Type Order
$\sigma_1$ is more general than $\sigma_2$ if there is a substitution $S$ that maps the for-all quantified
variables in $\sigma_1$, and $S(\sigma_1) = \sigma_2$.
That is essentially what generalization is: adding a $\forall$ quantifier to a free type variable in a type.
In HM we can only generalize a type when the type variable is not free in the context, so the signature
for generalize, $\mathcal{G}$ is
$$
\mathcal{G}(\Gamma, \sigma) = \textup{the most generalized version of the type }\sigma
$$
Where the upper part is called the premise, and the lower part the conclusion or judgement.
You can read this example as "if the assignment $\mathtt{x}:\sigma$ is in the context $\Gamma$then
from the context $\Gamma$ it follows that $\mathtt{x}$ has type $\sigma$." This is almost a tautology,
but a necessary one when specifying a type checking algorithm.
The VAR Rule
The first typing rule in HM is $\mathtt{VAR}$ for "variable" and is the one we just looked at:
You can read this as if from the context it follows that $\mathtt{e_0}$ has type $\tau_a \rightarrow \tau_b$and from the context $\mathtt{e_1}$ has type $\tau_a$then from the context it follows that the
application of $\mathtt{e_0}$ to $\mathtt{e_1}$ has type $\tau_b$, or mor colloquially "the application
of a function of type $\tau_a \rightarrow \tau_b$ to a type $\tau_a$ results in a $\tau_b$."
One point to note is that $\tau_a$ and $\tau_b$ are monotypes, this rule doesn't apply to polytypes ($\sigma$).
Says if from the context plus an assignment $\mathtt{x}$ has type $\tau_a$ it follows that $\mathtt{e}$ has type $\tau_b$,
then from the context it follows that expression $\lambda \mathtt{x} \rightarrow \mathtt{e}$ has type $\tau_a \rightarrow \tau_b$.
This is subtle, why the extra assigment outside of the context? and why from the context alone does it
follow that the function abstraction has that type? I think it's working backwards from the body of the
function abstraction to its argument type, and the $\mathtt{n}$ is only required as a placeholder for a
unifiable variable.
The LET Rule
There is a special rule for $\mathtt{let}$ bindings.
Says that if from the context it follows that $\mathtt{e_0}$ has type $\mathtt{sigma}$and
from the context plust a type assignment of $\sigma$ to $\mathtt{x}$ it follows that $\mathtt{e_1}$
has type $\tau$, then from the context alone it follows that $\mathtt{let\ x = e_0\ in\ e_1}$ has
type $\tau$.
Note that the result $\tau$ is constrained to be a monotype, this will be important later.
Also note that this is a kind of mixture of both the $\mathtt{APP}$ and $\mathtt{ABS}$ rules.
Says if$\mathtt{e}$ has type $\sigma$and$\alpha$ is not in the free variables of $\Gamma$then the type of $\mathtt{e}$ is actually $\forall\alpha . \sigma$.
Says if$\mathtt{things}$ has type $\mathtt{List}\ \alpha$and$\alpha$ is not in the free
variables of $\Gamma$then$\forall$-quantify $\mathtt{List}\ \alpha$ with $\alpha$.
The videos refer to This Paper by Lee and Yi, which uses a slightly different lambda calculus and formulation of the typing rules, so we start by reviewing those.
Most notable is the addition of a $\mathtt{[fix]}$ construct, which I believe is the pure functional equivalent of letrec, but I don't pretend to understand it and I have an alternative approach for handling letrec.
Type Schemes are what we've been calling polytypes.
The $\forall\vec{\alpha}$ here is just shorthand for $\forall\alpha_1.\forall\alpha_2.\forall\alpha_3\dots$
This is saying that applying $\mathcal{W}$ to a variable looks up the possibly quantified type of the variable in the context and returns it, with all of its quantifiers replaced with fresh type variables.
Applying $\mathcal{W}$ to a lambda expression first creates a fresh type variable $\beta$, then evaluates the body of the lambda $\mathtt{e}$ with a context extended by a mapping from $\mathtt{x}$ to $\beta$.
It then returns the substitution from the result, plus a function application type $\beta \rightarrow \tau$ (where $\tau$ is the type from the result) but with the substitution from the result applied to it.
So when applying $\mathcal{W}$ to a function application $\mathtt{e_1e_2}$, first (reading from bottom to top) calculate the substitution for and type of $\mathtt{e_1}$ in the current context: $(S_1, \tau_1)$. Next apply the substitution $S_1$ to the current context and use that new context to determine the substitution for, and type of $\mathtt{e_2}$: $(S_2, \tau_2)$. Then create a fresh type variable $\beta$ and a function application from the inferred type of $\mathtt{e_2}$ to that $\beta$, and unify that with the inferred type of $\mathtt{e_1}$ after applying the substitution $S_2$ to it. Finally return the combination of all the inferred substitutions plus the type resulting from applying $S_3$ to $\beta$.
When applying $\mathcal{W}$ to a let expression: $\mathtt{let\ x = e_1\ in\ e_2}$, first use the current context to determine the substitution for, and type of $\mathtt{e_1}$: $(S_1, \tau_1)$.
Use that substitution to modify the context, and then extend the context with a mapping from $\mathtt{x}$ to the polytype version of the type $\tau_1$, and use that context to infer the substitution for, and type of $\mathtt{e_2}$: $(S_2, \tau_2)$.
Return the type of $\mathtt{e_2}$ plus the combination of the two substitutions.
fix
We won't need this. My idea for typechecking letrec I think is ok:
When actually evaluating (with eval) a letrec we need to create an environment populated with
dummy variables, then replace those variables with their actual values as the letrec bindings are computed.
That way the functions in a letrec can "see" themselves and all their siblings when they actually execute.
Analogously when typechecking a letrec we create an extended context with each variable bound
to a fresh type variable. Those variables will be unified with the types of the letrec expressions appropriately.
Extensions
These are my modifications and additions to the above, to support the F-natural language. In F-natural functions can take multiple
arguments so the abstraction and application cases will need to change, plus we'll need a case for if.
Algorithm W Again
My changes and additions in $\color{blue}\text{blue}$.
Because in an arg like $\mathtt{x(y)}$ the $\mathtt{x}$ is to be treated as a type constructor and not bound.
if
Actually, for the purposes of typechecking, we can just treat if as a function with three arguments: $\mathtt{Bool} \rightarrow \beta \rightarrow \beta \rightarrow \beta$.
It takes a bool and two betas and produces a beta.