Define a PL: functions

Translations: English日本語

In the previous post, we introduced Hatsugen, a small programming language with integer and boolean types.

In this post, we’ll add functions to Hatsugen. With this addition, Hatsugen becomes approximately as powerful as the simply-typed lambda calculus.


We update the expression syntax to add variables, function literals, and function application. We also update the type syntax to add function types.

For variables, we just write things like xx or yy or x1x_1 or xx'. There are infinitely many variable names to choose from.

λ(x:τ) e\lambda (x: \tau) \ e is a function literal, taking one argument xx of type τ\tau and evaluating ee when applied to an argument. xx may appear in the expression ee.

e1(e2)e_1(e_2) is an application expression, representing the application of the function e1e_1 to the argument e2e_2.

τ1τ2\tau_1 \rightarrow \tau_2 is the type of functions taking τ1\tau_1 as input and returning τ2\tau_2 as output.

τ::=  τ1τ2e::=  x λ(x:τ) e e1(e2) \begin{aligned} \tau ::= \ & \dots \\ | \ & \tau_1 \rightarrow \tau_2 \\ \\ e ::= \ & \dots \\ | \ & x \\ | \ & \lambda (x: \tau) \ e \\ | \ & e_1(e_2) \end{aligned}

Statics: Γe:τ\Gamma \vdash e: \tau

Consider the expression λ(x:Int) x\lambda (x: \mathsf{Int}) \ x. It should have type IntInt\mathsf{Int} \rightarrow \mathsf{Int}.

The very similar expression λ(x:Bool) x\lambda (x: \mathsf{Bool}) \ x should have type BoolBool\mathsf{Bool} \rightarrow \mathsf{Bool}.

Notice that both of these example expressions contain the sub-expression xx, as the body of the function. But in each, the type of xx is different: Int\mathsf{Int} in the first and Bool\mathsf{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 xx) 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 Γ\Gamma 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:τ \begin{aligned} \Gamma ::= \ & \cdot \\ | \ & \Gamma, x: \tau \end{aligned}

The old typing judgement was e:τe: \tau, read “ee has type τ\tau”. The new judgement is written Γe:τ\Gamma \vdash e: \tau, read “Γ\Gamma entails ee has type τ\tau”.

We’ll need to update all the statics rules from the first post. All of these rules just use the context without changing it.

Γn:Int \frac {} {\Gamma \vdash \overline{n}: \mathsf{Int}} Γtrue:Bool \frac {} {\Gamma \vdash \mathsf{true}: \mathsf{Bool}} Γfalse:Bool \frac {} {\Gamma \vdash \mathsf{false}: \mathsf{Bool}} Γe1:BoolΓe2:τΓe3:τΓif e1 then e2 else e3:τ \frac { \Gamma \vdash e_1: \mathsf{Bool} \hspace{1em} \Gamma \vdash e_2: \tau \hspace{1em} \Gamma \vdash e_3: \tau } { \Gamma \vdash \mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3: \tau }

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)=τ\Gamma(x) = \tau.

(Γ,x:τ)(x)=τ \frac {} {(\Gamma, x: \tau)(x) = \tau} xyΓ(x)=τ(Γ,y:τ)(x)=τ \frac { x \ne y \hspace{1em} \Gamma(x) = \tau } {(\Gamma, y: \tau')(x) = \tau}

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 (\cdot, x: \mathsf{Int}, x: \mathsf{Bool}, y: \mathsf{Int})(x) = \mathsf{Bool}

We can now use this helper lookup judgement in the typing rule for variables.

Γ(x)=τΓx:τ \frac {\Gamma(x) = \tau} {\Gamma \vdash x: \tau}

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:τ1e:τ2Γλ(x:τ1) e:τ1τ2 \frac {\Gamma, x: \tau_1 \vdash e: \tau_2} {\Gamma \vdash \lambda (x: \tau_1) \ e: \tau_1 \rightarrow \tau_2}

For application, the parameter and argument types must match.

Γe1:τ1τ2Γe2:τ1Γe1(e2):τ2 \frac { \Gamma \vdash e_1: \tau_1 \rightarrow \tau_2 \hspace{1em} \Gamma \vdash e_2: \tau_1 } {\Gamma \vdash e_1(e_2): \tau_2}

Dynamics: e vale \ \mathsf{val} and eee \mapsto e'

Functions are values, regardless of whether the function body is a value:

λ(x:τ) e val \frac {} {\lambda (x: \tau) \ e \ \mathsf{val}}

For application expressions, we first step the function expression. Then, once it’s a value, we step the argument to a value as well:

e1e1e1(e2)e1(e2) \frac {e_1 \mapsto e_1'} {e_1(e_2) \mapsto e_1'(e_2)} e1 vale2e2e1(e2)e1(e2) \frac { e_1 \ \mathsf{val} \hspace{1em} e_2 \mapsto e_2' } {e_1(e_2) \mapsto e_1(e_2')}

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 [xex]e=e[x \mapsto e_x] e = e' to mean “substituting all free occurrences of xx with exe_x in ee yields ee'”.

e2 val[xe2]e=e(λ(x:τ) e) e2e \frac { e_2 \ \mathsf{val} \hspace{1em} [x \mapsto e_2] e = e' } { (\lambda (x: \tau) \ e) \ e_2 \mapsto e' }

Substitution: [xex]e=e[x \mapsto e_x] e = e'

To define the dynamics for function application, we must now define substitution for expressions.

Substitution does nothing to integer and boolean literals:

[xex]n=n \frac {} {[x \mapsto e_x] \overline{n} = \overline{n}} [xex]true=true \frac {} {[x \mapsto e_x] \mathsf{true} = \mathsf{true}} [xex]false=false \frac {} {[x \mapsto e_x] \mathsf{false} = \mathsf{false}}

For conditional and application expressions, we simply recurse on the sub-expressions:

[xex]e1=e1[xex]e2=e2[xex]e3=e3[xex]if e1 then e2 else e3=if e1 then e2 else e3 \frac { \begin{aligned} &[x \mapsto e_x] e_1 = e_1' \hspace{1em} \\&[x \mapsto e_x] e_2 = e_2' \hspace{1em} \\&[x \mapsto e_x] e_3 = e_3' \end{aligned} } { \begin{aligned} [x \mapsto e_x] &\mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 = \\&\mathsf{if} \ e_1' \ \mathsf{then} \ e_2' \ \mathsf{else} \ e_3' \end{aligned} } [xex]e1=e1[xex]e2=e2[xex]e1(e2)=e1(e2) \frac { [x \mapsto e_x] e_1 = e_1' \hspace{1em} [x \mapsto e_x] e_2 = e_2' } { [x \mapsto e_x] e_1(e_2) = e_1'(e_2') }

For variables, we case on whether the variable in the expression is the variable being substituted. If it is, we replace the variable with exe_x. If not, we leave it alone.

[xex]x=ex \frac {} {[x \mapsto e_x] x = e_x} xy[xex]y=y \frac {x \ne y} {[x \mapsto e_x] y = 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 Γ\Gamma.

[xex]λ(x:τ) e=λ(x:τ) e \frac {} {[x \mapsto e_x] \lambda (x: \tau) \ e = \lambda (x: \tau) \ e}

For the case when the variables are different, we must take care to avoid variable capture. For example, if we define

xy[xex]e=e[xex]λ(y:τ) e=λ(y:τ) e \frac { x \ne y \hspace{1em} [x \mapsto e_x] e = e' } {[x \mapsto e_x] \lambda (y: \tau) \ e = \lambda (y: \tau) \ e'}

we can use the rules to prove that

[xy]λ(y:Bool) x=λ(y:Bool) y[x \mapsto y] \lambda (y: \mathsf{Bool}) \ x = \lambda (y: \mathsf{Bool}) \ y

In this case, the variable yy has been captured by the binding for yy in the function literal.

To avoid this, we require that the variable bound by the function literal not appear free in exe_x. We thus revise the rule, writing fv(ex)\mathsf{fv}(e_x) to denote the free variables in exe_x.

xyyfv(ex)[xex]e=e[xex]λ(y:τ) e=λ(y:τ) e \frac { x \ne y \hspace{1em} y \notin \mathsf{fv}(e_x) \hspace{1em} [x \mapsto e_x] e = e' } {[x \mapsto e_x] \lambda (y: \tau) \ e = \lambda (y: \tau) \ e'}

Free variables: fv(e)\mathsf{fv}(e)

We must now define the free variables of an expression.

Integer and boolean literals have no free variables:

fv(n)= \frac {} {\mathsf{fv}(\overline{n}) = \emptyset} fv(true)= \frac {} {\mathsf{fv}(\mathsf{true}) = \emptyset} fv(false)= \frac {} {\mathsf{fv}(\mathsf{false}) = \emptyset}

For conditional and application expressions, we simply recurse and union:

fv(e1)=s1fv(e2)=s2fv(e3)=s3fv(if e1 then e2 else e3)=s1s2s3 \frac { \mathsf{fv}(e_1) = s_1 \hspace{1em} \mathsf{fv}(e_2) = s_2 \hspace{1em} \mathsf{fv}(e_3) = s_3 } { \mathsf{fv}(\mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3) = s_1 \cup s_2 \cup s_3 } fv(e1)=s1fv(e2)=s2fv(e1(e2))=s1s2 \frac { \mathsf{fv}(e_1) = s_1 \hspace{1em} \mathsf{fv}(e_2) = s_2 } { \mathsf{fv}(e_1(e_2)) = s_1 \cup s_2 }

Variables alone are free:

fv(x)={x} \frac {} {\mathsf{fv}(x) = \{ x \}}

Function literals bind a single variable:

fv(e)=sfv(λ(x:τ) e)=s{x} \frac {\mathsf{fv}(e) = s} {\mathsf{fv}(\lambda (x: \tau) \ e) = s \setminus \{ x \}}


Since the judgments have changed a bit, we’ll need to restate the theorems slightly.


For all Γ\Gamma and ee and τ\tau, if Γe:τ\Gamma \vdash e: \tau and fv(e)=\mathsf{fv}(e) = \emptyset, then e vale \ \mathsf{val} or there exists ee' such that eee \mapsto e'.

We require that ee have no free variables at all. This will allow us to perform substitution as we evaluate.

To see why this is necessary, consider choosing ee to be

(λ(x:BoolBool) x) (λ(y:Bool) x) (\lambda (x: \mathsf{Bool} \rightarrow \mathsf{Bool}) \ x) \ (\lambda (y: \mathsf{Bool}) \ x)

This expression has one free variable, xx. According to the rules, this expression is neither a value nor can it step. This is because xx appears free in the argument but is bound by the function being applied.

The expression xx is an even smaller counterexample, since bare variables are neither values nor can they step. Variables are given meaning by substitution.


For all Γ\Gamma and ee and ee' and τ\tau, if Γe:τ\Gamma \vdash e: \tau and fv(e)=\mathsf{fv}(e) = \emptyset and eee \mapsto e', then Γe:τ\Gamma \vdash e': \tau and fv(e)=\mathsf{fv}(e') = \emptyset.

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 ee' in order to be able to feed ee' back into the progress theorem.


Once again, taken together we have the following safety theorem:

For all Γ\Gamma and ee and τ\tau, if Γe:τ\Gamma \vdash e: \tau and fv(e)=\mathsf{fv}(e) = \emptyset, then e vale \ \mathsf{val} or there exists ee' such that eee \mapsto e' and Γe:τ\Gamma \vdash e': \tau and fv(e)=\mathsf{fv}(e') = \emptyset.

The proofs are once again on GitHub.

In the next post, we’ll add product types, also known as structs or tuples.