Exercise 3.1
How many λ2-contexts are there consisting of the four declarations?
$$α : ∗$$
$$β : ∗$$
$$f : α →β$$
$$x : α$$
Definition 3.4.4 defines λ2 contexts:
(1) $∅$ is a λ2-context; $dom(∅) = ()$, the empty list.
(2) If $Γ$ is a λ2-context, $α ∈V$ and $α \notin dom(Γ)$, then $Γ, α : ∗$ is a λ2-context; $dom(Γ,α : ∗) = (dom(Γ), α)$, i.e. $dom(Γ)$ concatenated with $α$.
(3) If $Γ$ is a λ2-context, if $ρ ∈\mathbb{T}2$ such that $α ∈dom(Γ)$ for all free type variables $α$ occurring in $ρ$ and if $x \notin dom(Γ)$, then $Γ, x : ρ$ is a λ2-context; $dom(Γ,x : ρ) = (dom(Γ), x)$.
Using this definition we have the following possibilities for valid λ2-contexts:
- $α : * \quad$ by (2)
- $α : *, \; x : α \quad$ by (3)
- $β : * \quad$ by (2)
- $α: *, \; β : * \quad$ by (2)
- $α: *, \; β : *, \; f: α→β \quad$ by (3)
- $α : *, β : *, \; x: α \quad$ by (3)
- $α : *, β : *, \; x: α, \; f:α→β \quad$ by (3)
Note that some declarations don't make for valid λ2-contexts, eg $x:α$ and $f:α→β$, because they use type variables that have not been established in the context.
