Consider the expression λ(x:Int)x. It should have type Int→Int.
The very similar expression λ(x:Bool)x should have type Bool→Bool.
Notice that both of these example expressions contain the sub-expression x, as the body of the function. But in each, the type of x is different: Int in the first and Bool in the second.
As this example illustrates, the type of variables is determined by how the variable is declared. This is the first time that the same expression (in this case x) can have a different type depending on the context.
We’ll need to fundamentally change the structure of the static semantics to account for variables.
First, we’ll need to formalize the notion of a context. We’ll use Γ to represent a context, which will just be a list of variable-type pairs.
A context can either be empty, or it can be an existing context augmented with a new variable-type pair.
Γ::=∣⋅Γ,x:τ
The old typing judgement was e:τ, read “e has type τ”. The new judgement is written Γ⊢e:τ, read “Γ entails e has type τ”.
We’ll need to update all the statics rules from the first post. All of these rules just use the context without changing it.
We can now add the typing rules for the new constructs.
For variables, we need to be able to look up the variable in question in the context to get its type. For that, we’ll define a small helper judgement for context lookup, written Γ(x)=τ.
(Γ,x:τ)(x)=τ(Γ,y:τ′)(x)=τx=yΓ(x)=τ
Note that these rules engender shadowing, which is where multiple variable-type pairs with the same variable exist in the context at once, but the one furthest to the right in the context determines the type of the variable under the context. For instance, using the rules we can derive
(⋅,x:Int,x:Bool,y:Int)(x)=Bool
We can now use this helper lookup judgement in the typing rule for variables.
Γ⊢x:τΓ(x)=τ
For function literals, the type of the parameter is the input type, and the type of the function body is the output type.
However, the bound variable may appear in the function body. So we add the variable and its type to the context when determining the function body’s type.
Γ⊢λ(x:τ1)e:τ1→τ2Γ,x:τ1⊢e:τ2
For application, the parameter and argument types must match.
Once both expressions are values, we can prove the first will be a function literal, since it had function type.
We will step into the body of the function, substituting all free occurrences of the variable bound by the function with the value of the argument. We write [x↦ex]e=e′ to mean “substituting all free occurrences of x with ex in e yields e′”.
For variables, we case on whether the variable in the expression is the variable being substituted. If it is, we replace the variable with ex. If not, we leave it alone.
[x↦ex]x=ex[x↦ex]y=yx=y
For function literals, we again case on whether the variables are the same. If they are, we leave the function literal untouched. This is consistent with how we treat variables with the same name in the context Γ.
[x↦ex]λ(x:τ)e=λ(x:τ)e
For the case when the variables are different, we must take care to avoid variable capture. For example, if we define
[x↦ex]λ(y:τ)e=λ(y:τ)e′x=y[x↦ex]e=e′
we can use the rules to prove that
[x↦y]λ(y:Bool)x=λ(y:Bool)y
In this case, the variable y has been captured by the binding for y in the function literal.
To avoid this, we require that the variable bound by the function literal not appear free in ex. We thus revise the rule, writing fv(ex) to denote the free variables in ex.
For all Γ and e and τ, if Γ⊢e:τ and fv(e)=∅, then eval or there exists e′ such that e↦e′.
We require that e have no free variables at all. This will allow us to perform substitution as we evaluate.
To see why this is necessary, consider choosing e to be
(λ(x:Bool→Bool)x)(λ(y:Bool)x)
This expression has one free variable, x. According to the rules, this expression is neither a value nor can it step. This is because x appears free in the argument but is bound by the function being applied.
The expression x is an even smaller counterexample, since bare variables are neither values nor can they step. Variables are given meaning by substitution.
For all Γ and e and e′ and τ, if Γ⊢e:τ and fv(e)=∅ and e↦e′, then Γ⊢e′:τ and fv(e′)=∅.
Preservation not only preserves typing, but also the presence of free variables. This is important, since we need there to be no free variables in e′ in order to be able to feed e′ back into the progress theorem.