Chapter 9 of TaPL describes a
simple language consisting of lambda calculus (from chapter 5) plus the boolean
expressions true
, false
, and if ... then ... else ...
(from chapters 3 and
8).
It then shows how that language can by typed. This Simply Typed Lambda Calculus forms the basis of every other typed language in the rest of the book.
We can say that true
and false
have the type Bool
. But what is the type of
a function? We could give them a type called Function
, which we will spell →
for brevity, but that's not very useful. Too many different functions would be
lumped together in the same type. To be useful we need to know the type returned
by the function and what type of argument it expects. We will spell that T₁→T₂
where T₁ is the type of the argument and T₂ the type of the result. So we have
the grammar rule:
T ::=
Bool
T → T
With Bool
as our only base type that gives us an infinite family of function
types:
Bool→Bool
(Bool→Bool)→Bool
Bool→(Bool→Bool)
(Bool→Bool)→(Bool→Bool)
→
is right associative so Bool→Bool→Bool
means Bool→(Bool→Bool)
.
There are two approaches to assigning a type to a function (lambda abstraction) such as:
(λ.x if x then false else true)
The clever way is to analyse the body of the function and deduce that x has to be a Bool. That's covered in Chapter 22.
The simpler way - which is the one used in this chapter - is just to annotate the function with the intended type:
(λ.x:Bool if x then false else true)
Chapter 8 introduced the binary typing relation ":"
which is used in
expressions like "t : T"
and can be read "term t
has type T
". The
introduction of lambda calculus variables complicates things. The type of a term
can depend on the types of variables used in that term. That changes the typing
relation from a binary one to a ternary one "⊢ :"
which is used in expressions
like "Γ ⊢ t : T"
and which can be read "Given the typing context Γ
(gamma)
we can infer that the term t
has type T
".
The typing context Γ
is sequence of (variable_name, type) pairs. However, it
can also be thought of as an associative array (dict, map, hashtable) or a
function from the name of a variable to its type. An empty context can be
written ∅ or omitted as in "⊢ t : T"
. Contexts can be extended using a comma
so "Γ, x:T₁"
is the typing context containing everything in Γ plus the
variable x which is of type T₁. Contexts also support set membership so
"x:T ∈ Γ"
means "The type assigned to x
in Γ
is T
".
Given all that we're now in a position to define the typing rules for the simply typed lambda calculus as follows:
import re
import inference
from inference import Rule, Syntax
class SimplyTypedLambdaCalculus(inference.Rules):
## SYNTAX
# This grammar differs slightly from what's in the book. I'm using a
# recursive decent parser so I need to avoid left-recursive productions.
# I do that in term and type by introducing termʹ and typeʹ and doing the
# usual transformations to remove the left-recursion.
rule = Syntax(
'{term} ⟶ {term}',
'{context} ⊢ {term} : {type}',
'{var} : {type} ∈ {context}',
)
term = Syntax(
'( {term} ) {termʹ}',
'true {termʹ}',
'false {termʹ}',
'if {term} then {term} else {term} {termʹ}',
'{var} {termʹ}',
'λ {var} : {type} . {term} {termʹ}',
)
termʹ = Syntax(
'{term} {termʹ}',
'',
)
var = Syntax(
re.compile(r"[a-z]('+|\b)")
)
type = Syntax(
'( {type} ) {typeʹ}',
'{base_type} {typeʹ}',
)
typeʹ = Syntax(
'→ {type} {typeʹ}',
'',
)
base_type = Syntax(
'Bool',
)
context = Syntax(
'( {context} )',
'∅',
'{var} : {type} , {context}'
)
## Lambda Calculus Typing
T_VAR = Rule('{Γ} ⊢ {x}:{T}', given=[
'{x}:{T} ∈ {Γ}'
])
T_ABS = Rule('{Γ} ⊢ λ{x}:{T1}.{t2} : {T1}→{T2}', given=[
'{x}:{T1},{Γ} ⊢ {t2} : {T2}',
])
T_APP = Rule('{Γ} ⊢ {t1} {t2} : {T12}', given=[
'{Γ} ⊢ {t1} : {T11}→{T12}',
'{Γ} ⊢ {t2} : {T11}',
])
## Boolean Typing
T_TRUE = Rule('{Γ} ⊢ true : Bool')
T_FALSE = Rule('{Γ} ⊢ false : Bool')
T_IF = Rule('{Γ} ⊢ if {t1} then {t2} else {t3} : {T}', given=[
'{Γ} ⊢ {t1} : Bool',
'{Γ} ⊢ {t2} : {T}',
'{Γ} ⊢ {t3} : {T}',
])
## List Membership
M_HEAD = Rule('{x}:{T} ∈ {x}:{T}, {Γ}')
M_TAIL = Rule('{x}:{T} ∈ {y}:{T1}, {Γ}', given=[
'{x}:{T} ∈ {Γ}',
])
@classmethod
def infer_type(cls, expression, context='∅'):
goal = f'{context} ⊢ {expression} : {{__result__}}'
return cls.solve(goal)
We're now in the position that we can infer the types of expressions
SimplyTypedLambdaCalculus.infer_type('(λx:Bool.x) true')
(Bool)
We can also draw the derivation trees of those proofs
SimplyTypedLambdaCalculus.infer_type('(λx:Bool.x) true').proof
|
| ||||||
∅ ⊢ ((λ x : Bool . x) true) : Bool |
The pure simply typed lambda calculus is the simply typed lambda calculus without anything related to the boolean base type. That's a useful thing to have as a base to build on, but in itself it is degenerate, meaning that it has no well-typed terms at all. The reason for that is that types in the pure simply typed lambda calculus have the form:
T = T→T
But with no base types to "prime the pumps" that results in there being no types in the language at all.
Draw a derivation tree for "f:(Bool→Bool) ⊢ f (if false then true else false) : Bool"
expression = 'f (if false then true else false)'
context = 'f:(Bool→Bool), ∅'
T = SimplyTypedLambdaCalculus.infer_type(expression, context=context)
assert T == ('Bool',)
T.proof
|
| ||||||||||||
(f : (Bool → Bool) , ∅) ⊢ (f (if false then true else false)) : Bool |
Draw a derivation tree for "f:(Bool→Bool) ⊢ λx:Bool. f(if false then true else false) : Bool→Bool"
expression = 'λx:Bool. f(if false then true else false)'
context = 'f:(Bool→Bool), ∅'
T = SimplyTypedLambdaCalculus.infer_type(expression, context=context)
assert T == ('Bool','→', 'Bool')
T.proof
| ||||||||||||||||||
(f : (Bool → Bool) , ∅) ⊢ (λ x : Bool . (f (if false then true else false))) : (Bool → Bool) |
Find a context Γ under which the term "f x y"
has the type Bool.
It would be lovely if we could show this by running:
SimplyTypedLambdaCalculus.solve('{context} ⊢ (f x y) : Bool')
and seeing what pops out. Unfortunately that doesn't work. Turns out that a few dozen lines of hastily written code for drawing derivation trees != Prolog. Who knew?
This is where TaPL proves that the Simply Typed Lambda Calculus is Type Safe. The proof follows the same lines as chapter 8. i.e.
Safety = Progress + Preservation.
"⊢ t : T"
then either t
is a value or there is some tʹ
where t ⟶ tʹ
"Γ ⊢ t : T"
and t ⟶ tʹ
then "Γ ⊢ tʹ : T"
Or in english:
I'm not going to reproduce the proofs here. They are can mostly be summarised as "sprinkle some induction on it". For more details, go read the book.
Can we construct a Γ
and T
such that "Γ ⊢ x x : T"
?
No, not with our current type system. The T-ABS
rule is the one which would
apply to that term. It says that the first x
has type T₁→T₂
and the second
x
has type T₁
. But since both x
s are the same its need to have both of
those types at the same time. Theres no way to unify T₁→T₂
with T₁
to make
that true.
Does "subject expansion" hold for the functional part of the calculus?
That is, Do "t ⟶ tʹ"
and "Γ ⊢ tʹ : T"
together imply "Γ ⊢ t : T"
for
terms t which don't include conditional expressions?
No. There exist untyped terms which evaluate to typed terms. For example.
(λx:Bool. λy.Bool. y)(true true)
expression1 = '(λx:Bool. λy:Bool. y)(true true)'
try:
T = SimplyTypedLambdaCalculus.infer_type(expression1)
print(f'The type of {expression1} is {T}')
except inference.NoProofFoundError:
print(f'{expression1} is not well-typed')
expression2 = '(λy:Bool. y)'
print(f'{expression1} evaluates to {expression2}')
try:
SimplyTypedLambdaCalculus.infer_type(expression2)
print(f'The type of {expression2} is {T}')
except inference.NoProofFoundError:
print(f'{expression2} is not well-typed')
(λx:Bool. λy:Bool. y)(true true) is not well-typed (λx:Bool. λy:Bool. y)(true true) evaluates to (λy:Bool. y) The type of (λy:Bool. y) is Bool → Bool
We skipped this because time was short and it seemed like an aside.
There were a couple of related talks recommended on slack before the meeting:
"Propositions as Types" - Philip Wadler
"The Hitchhiker's Guide to the Curry-Howard Correspondence" - Chris Ford
Even though we can define evaluation rules on typed terms, the type annotations play no role in the evaluation at runtime. They are carried along but are redundant.
Erasure is a function which maps simply typed terms to the equivalent terms in the untyped lambda calculus.
It can be proved that the following two approaches to evaluation are exactly equivalent:
Typability is in some ways the opposite of erasure. An untyped term m
is
said to be typable is there is some typed term t
, type T
and context Γ
such that
Γ ⊢ t : T and erase(t) = m
There are two ways of discussing the semantics of a typed language: