Chapter 3 - Exercise 21

Exercise 3.21

Give a recursive definition for $FTV(A)$, the set of free type variables in $A$, for an expression $A$ in $\mathbb{T}2$ or in $Λ_{\mathbb{T}2}$.

Let's remind ourselves of the recursive definition for free variables in untyped λ-terms.

Definition 1.4.1 ($FV$, the set of free variables of a λ-term)

(1) (Variable) $FV(x) = \{x\}$

(2) (Application) $FV(MN) = FV(M)∪FV(N)$

(3) (Abstraction) $FV(λx. M) = FV(M) \{x\}$

Let's also remind ourselves of the sets $\mathbb{T}2$ and $Λ_{\mathbb{T}2}$.

$\mathbb{T}2 = \mathbb{V} |(\mathbb{T}2 →\mathbb{T}2) |(Π\mathbb{V} : ∗. \mathbb{T}2)$

$Λ_{\mathbb{T}2} = V|(Λ_{\mathbb{T}2}Λ_{\mathbb{T}2})|(Λ_{\mathbb{T}2}\mathbb{T}2)|(λV : \mathbb{T}2. Λ_{\mathbb{T}2})|(λ\mathbb{V} : ∗. Λ_{\mathbb{T}2})$

Our recursive definition will need to cover all these cases. In the following section we'll consider each case.

$A$ in $\mathbb{T}2$, the λ2 Types

Let's consider the syntax cases for λ2 types.

• $\mathbb{V}$. These are type variables, for which we usually use lower case greek symbols, eg $α, β, γ$. In this case the type variable is free, and so $$FTV(α)=\{α\}$$
• $(\mathbb{T}2 →\mathbb{T}2)$. These are arrow types between other type variables, for example $α→β$. In this case the free type variables are those in the "from" and "to" expressions. So $$FTV(M→N)=FTV(M) \cup FTV(N)$$
• $(Π\mathbb{V} : ∗. \mathbb{T}2)$. These are the abstractions over a single type variable. An example is $Πα:*.α→Mα$. In this case, the abstracted variable is bound, not free, and so $$FTV(Πα:*.M) = FTV(M) \setminus \{α\}$$

$A$ in $Λ_{\mathbb{T}2}$, the Pre-Typed λ2 Terms

Let's now consider the syntax cases for the pre-typed λ2-terms.

• $V$. This is the simple case of a single term variable annotated with a type, eg $x$. These variables are pre-typed, and so the expression $x$ has no type variables in it. This means $$FTV(x)=\emptyset$$
• $(Λ_{\mathbb{T}2}Λ_{\mathbb{T}2})$. This is the application of one term to another, for example $MN$. Here we have $$FTV(MN)=FTV(M) \cup FTV(N)$$
• $(Λ_{\mathbb{T}2}\mathbb{T}2)$. This is the application of a term to a type, for example $Mα$. In this case $α$ is free, and so we have $$FTV(Mα)=FTV(M) \cup \{α\}$$
• $(λV : \mathbb{T}2. Λ_{\mathbb{T}2})$. This is an abstraction over a term variable, for example $λx.M$. Since $x$ is not a type variable, we have $$FTV(λx.M)=FTV(M)$$
• $(λ\mathbb{V} : ∗. Λ_{\mathbb{T}2})$. This is an abstraction over a type variable, for example $λα.M$. Here $α$ is not free, and so $$FTV(λα.M) = FTV(M) \setminus \{α\}$$

Recursive Definition

λ2 Types

• (Type Variable) $FTV(α)=\{α\}$
• (Arrow Type) $FTV(M→N)=FTV(M) \cup FTV(N)$
• (Abstraction) $FTV(Πα:*.M) = FTV(M) \setminus \{α\}$

λ2 Terms

• (Term Variable) $FTV(x)=\emptyset$
• (Application to term) $FTV(MN)=FTV(M) \cup FTV(N)$
• (Application to type) $FTV(Mα)=FTV(M) \cup \{α\}$
• (Abstraction of term) $FTV(λx.M)=FTV(M)$
• (Abstraction of type) $FTV(λα.M) = FTV(M) \setminus \{α\}$