Plan for this week
Past month:
How do we implement a tiny functional language?
Interpreter: how do we evaluate a program given its AST?
Parser: how do we convert strings to ASTs?
REPL: how do we write an app that repeatedly evaluates expressions?
This week:
How do we reason about programs mathematically?
Operational semantics: formalizing how programs evaluate
Type system: formalizing which expressions have which types
Type soundness: proving that well-typed programs behave well at run time
Type Checking: Goal
Consider a simplified version of Nano without:
let
-bindings- subtraction, multiplication, …
- booleans
- recursion
Expressions:
e ::= n -- numeral
| x -- variable
| e1 + e2 -- addition
| \x -> e -- abstraction
| e1 e2 -- application
Can you give me examples of Nano programs that crash? Run forever?
The goal of type checking is to detect and reject such programs before run.
QUIZ
Which one of these Nano programs is well-typed (in your opinion)?
(A) x + 1
(B) 1 2
(C) (\x -> x + 1) (\y -> y)
(D) (\f y -> f y) (\x -> x + 1) 5
(E) (\x -> x x) (\y -> y y)
Answer: D.
(A) x + 1
Type error: Unbound variable x
(B) 1 2
Type error: LHS of application should be of type Int -> T2
(C) (\x -> x + 1) (\y -> y)
Type error: RHS of application should be of type Int
(D) (\f y -> f y) (\x -> x + 1) 5 :: Int
(E) (\x -> x x) (\y -> y y)
Type error: x
cannot be both T1 -> T2
and T1
At run time:
- Programs A, B, C crash
- Program E runs forever
- Program D evaluates to a value (6)
Can we prove that all well-typed programs always evaluate to a value?
- do not crash?
- do not run forever?
Yes we can!
Outline
- Operational Semantics
- Type System
- Type Soundness
Nano: Operational Semantics
Operational semantics defines how to evaluate a program
- Like our
eval :: Env -> Expr -> Value
, but written in math
Let’s define an evaluation relation E ; e ==> v
- Informal meaning: “expression
e
evaluates to valuev
in environmentE
”
First we need to define values and environments:
Values:
v ::= n -- numeral
| <E, x, e> -- closure
Environments:
E ::= [] -- empty
| x := v, E -- value binding and rest
Inference Rules
In PL, we define relations formally using inference rules of the form:
premise_1 ... premise_n
[Rule-Name] -----------------------
conclusion
Meaning:
- If `premise_1` is true and ... and `premise_n` is true
- then `conclusion` is also true.
Or alternatively:
- In order to prove `conclusion`
- you have to prove `premise_1` and ... and `premise_n`.
Rules with no premises are called axioms
- Conclusion is *always* true
Nano Evaluation Rules
-- A numeral always evaluates to itself:
[E-Num] -------------
E ; n ==> n
-- A variable x evaluates to v in an env where it is bound to v:
[E-Var] --------------------
(x:=v,E) ; x ==> v
-- If both sides of addition evaluate to numerals,
-- then addition evaluated to their sum:
E ; e1 ==> n1 E ; e2 ==> n2 n == n1 + n2
[E-Add] --------------------------------------------
E ; (e1 + e2) ==> n
-- A lambda abstraction always evaluates to a closure:
[E-Lam] ---------------------------
E ; (\x -> e) ==> <E, x, e>
-- If LHS evaluates to a closure, RHS evaluates to v2,
-- and the body of the closure evaluates to v
-- in the closure environment extended with binding of formal to v2,
-- then the application of LHS to RHS evaluates to v:
E ; e1 ==> <E', x, e> E ; e2 ==> v2 (x:=v2,E') ; e ==> v
[E-App] ---------------------------------------------------------------
E ; (e1 e2) ==> v
Derivations
A derivation of E ; e ==> v
is a tree build from inference rules where
- the root is
E ; e ==> v
- leaves are axioms
For example, this is the derivation of ([x:=5], x + 1) ==> 6
[E-Var] ---------------- [E-Num]---------------
[x:=5] ; x ==> 5 [x:=5] ; 1 ==> 1 6 == 1 + 5
[E-Add] --------------------------------------------------
[x:=5] ; (x + 1) ==> 6
Meaning:
- Our goal is to prove that
[x:=5] ; (x + 1) ==> 6
. - This relation matches the conclusion of rule
[E-Add]
. - Hence we can construct its derivation using
[E-Add]
, we only need to prove its premises. - The first premise is
[x:=5] ; x ==> n1
:- This relation matches the conclusion of rule
[E-Var]
. - Hence we can construct its derivation using
[E-Var]
withn1 == 5
. [E-Var]
has no premises, hence this sub-derivation is complete.
- This relation matches the conclusion of rule
- The second premise is
[x:=5] ; 1 ==> n2
:- This relation matches the conclusion of rule
[E-Num]
. - Hence we can construct its derivation using
[E-Num]
withn2 == 1
. [E-Num]
has no premises, hence this sub-derivation is complete.
- This relation matches the conclusion of rule
- Since
6 == 5 + 1
, we conclude[x:=5] ; (x + 1) ==> 6
by[E-Add]
.
QUIZ
What is the correct derivation of [] ; (1 + 2) + 3 ==> 6
?
(A)
6==1+2+3
[E-Add] ------------------------
[] ; (1 + 2) + 3 ==> 6
(B)
[E-Num] [E-Num] [E-Num]
---------- ---------- ----------
[];1 ==> 1 [];2 ==> 2 [];3 ==> 3 6==1+2+3
[E-Add]---------------------------------------------
[] ; (1 + 2) + 3 ==> 6
(C)
[E-Num] [E-Num]
---------- ----------
[];1 ==> 1 [];2 ==> 2 3==1+2 [E-Num]
[E-Add]-------------------------------- ----------
[];(1 + 2) ==> 3 [];3 ==> 3 6==3+3
[E-Add]------------------------------------------------------
[] ; (1 + 2) + 3 ==> 6
Answer: C.
QUIZ
Which of the following relations have a derivation for some value v
?
(A) [] ; x + 1 ==> v
(B) [] ; 1 2 ==> v
(C) [] ; (\f y -> f y) (\x -> x + 1) ==> v
(D) [] ; (\x -> x x) (\y -> y y) ==> v
Answer: C.
(A)
-- NO RULE MATCHES!!!
--------------
[] ; x ==> n1 ... ...
[E-Add]-----------------------------
[] ; x + 1 ==> v
(B)
-- NO RULE MATCHES!!!
------------------
[] ; 1 ==> <E,x,e> ... ...
[E-App]------------------------------
[] ; 1 2 ==> v
(C)
[E-Lam]
------------------------------------------------------
[f:=<[],x,x+1>] ; \y->f y ==> <[f:=<[],x,x+1>],y,f y>
^
[E-Lam] [E-Lam] |
----------------------------------- ------------------------------- |
[];(\f y -> f y) ==> <[],f,\y->f y> [];(\x -> x + 1) ==> <[],x,x+1> |
[E-App]-----------------------------------------------------------------
[] ; (\f y -> f y) (\x -> x + 1) ==> v
(D)
-- X2 AND SO ON!
[E-Var] ---------------------------------- ----------------------------
[x:=<[],x,x x>] ; x ==> <[],x,x x> [x:=<[],x,x x>] ; x x ==> v
[E-App]------------------------------------------------
[x:=<[],x,x x>] ; x x ==> v
-- X2
[E-Lam]-----------------------------
[];(\x -> x x) ==> <[],x,x x>
[E-App]----------------------------------------------------------
[] ; (\x -> x x) (\x -> x x) ==> v
Evaluation Results
For any pair E ; e
one of the following is true:
We can build a derivation
E ; e ==> v
for somev
- We say that
e
evaluates to a value inE
- Example:
[x:=5] ; (x + 1) ==> 6
- We say that
We try to build a derivation, but at some point no rule applies
- We say that
e
gets stuck inE
(corresponds to runtime error / crash ineval
) - Example:
[] ; (x + 1)
- We say that
We try to build a derivation, but it just goes on forever
- We say that
e
diverges inE
(corresponds to nontermination ineval
) - Example:
[] ; (\x -> x x) (\y -> y y)
- We say that
In cases 2 and 3 we say that e
goes wrong in E
.
Outline
- Operational Semantics [done]
- Type System
- Type Soundness
Type System for Nano
A type system defines what types we can assign to an expression
Let’s try to define a typing relation e :: T
- Informal meaning: “expression
e
has typeT
”
First we need to define what types look like:
Types:
T ::= Int -- integers
| T1 -> T2 -- function types
Typing Rules: Take I
We define the typing relation using inference rules:
-- A numeral always has type Int:
[T-Num] n :: Int
-- Addition has type Int, provided both sides have type Int:
e1 :: Int e2 :: Int
[T-Add] ----------------------
e1 + e2 :: Int
-- Variable has type ???
[T-Var] x :: ???
What is the type of a variable?
Reminder: to evaluate a variable we save its value in the environment
So: to type a variable we have to save its type in the type environment
Type Environment
An expression has a type in a given type environment (also called context), which maps all its free variables to their types
Contexts:
G ::= [] -- empty
| x:T, G -- type binding and rest
Our typing relation should include the context G |- e :: T
:
- Informal meaning: “expression
e
has typeT
in contextG
”
Typing rules
-- A numeral always has type Int:
[T-Num] -------------
G |- n :: Int
-- A variable has type T in a context that binds it to T:
[T-Var] ----------------
x:T, G |- x :: T
-- Addition has type Int, provided both sides have type Int:
G |- e1 :: Int G |- e2 :: Int
[T-Add] -------------------------------
G |- e1 + e2 :: Int
-- Lambda abstraction has type T1 -> T2 provided
-- its body has type T2 in a context where formal is bound to T1:
x:T1, G |- e :: T2
[T-Lam] ------------------------
G |- \x -> e :: T1 -> T2
-- Application has type T2 provided there exists T1
-- such that the LHS has type T1 -> T2 and RHS has type T1
G |- e1 :: T1 -> T2 G |- e2 :: T1
[T-App] -----------------------------------
G |- e1 e2 :: T2
An expression e
has type T
in G
if we can derive G |- e :: T
using these rules
An expression e
is well-typed in G
if we can derive G |- e :: T
for some type T
- and ill-typed otherwise
For example, this is the derivation of [x:=5] |- x + 1 :: Int
[T-Var] ----------------- [T-Num]----------------
[x:=5] ; x :: Int [x:=5] ; 1 :: Int
[T-Add] ------------------------------------------
[x:=5] |- x + 1 :: Int
Meaning:
- Our goal is to prove that
[x:=5] |- x + 1 :: Int
. - This relation matches the conclusion of rule
[T-Add]
. - Hence we can construct its derivation using
[T-Add]
, we only need to prove its premises. - The first premise is
[x:=5] ; x :: Int
:- This relation matches the conclusion of rule
[T-Var]
. [T-Var]
has no premises, hence this sub-derivation is complete.
- This relation matches the conclusion of rule
- The second premise is
[x:=5] ; 1 :: Int
:- This relation matches the conclusion of rule
[T-Num]
. [T-Num]
has no premises, hence this sub-derivation is complete.
- This relation matches the conclusion of rule
QUIZ
What is the correct derivation of [] |- (\x -> x) 2 :: Int
?
(A)
[T-Num] ------------------------
[] |- 2 :: Int
[T-App] ------------------------
[] |- (\x -> x) 2 :: Int
(B)
[T-Num] --------------------
[x := 2] |- 2 :: Int
[T-Var] --------------------
[x := 2] |- x :: Int
[T-App] ------------------------
[] |- (\x -> x) 2 :: Int
(C)
[T-Var] -------------------
[x:Int] |- x :: Int
[T-Lam] --------------------------- -------------- [T-Num]
[] |- \x -> x :: Int -> Int [] |- 2 :: Int
[T-App] -----------------------------------------------
[] |- (\x -> x) 2 :: Int
Answer: C.
QUIZ
Which of the following typing relations have a derivation for some type T
?
(A) [] |- x + 1 :: T
(B) [] |- 1 2 :: T
(C) [] |- \x -> x x :: T
(D) [] |- (\f y -> f y) (\x -> x + 1) :: T
Answer: D.
(A)
-- NO RULE MATCHES!!!
--------------
[] |- x :: Int ...
[T-Add]-----------------------
[] |- x + 1 :: T
(B)
-- NO RULE MATCHES!!!
------------------
[] |- 1 :: T1 -> T2 ...
[T-App]--------------------------
[] |- 1 2 :: T
(C)
-- CAN'T FIND T1 = (T3 -> T2) = T3
[x:T1] |- x :: T3 -> T2 [x:T1] |- x :: T3
[T-App]-------------------------------------------
[x:T1] |- x x :: T2
[T-Lam]-----------------------------
[] |- \x -> x x :: T1 -> T2
(D)
[T-Var]----------- -------------[T-Var]
[...]|-f::Int->Int [...]|-y::Int
[T-App]------------------------- [T-Var]-------- [T-Num]---------
[y:Int,f:Int->Int] |- f y :: Int [x:Int]|-x::Int [x:Int]|-1::Int
[T-Lam]------------------------------ ----------------------[T-Add]
[f:Int->Int] |- \y -> f y :: Int->Int [x:Int] |- x + 1 :: Int
[T-Lam]---------------------------------- ----------------------[T-Lam]
[] |- \f y -> f y :: (Int->Int)->Int->Int [] |- \x -> x + 1 :: Int->Int
[T-App]-----------------------------------------------------------------
[] |- (\f y -> f y) (\x -> x + 1) :: Int->Int
Outline
- Operational Semantics [done]
- Type System [done]
- Type Soundness
Well-Typed Programs Always Succeed
We would like to prove the following theorem:
Theorem (Well-Typed Programs Always Succeed): For any program e
and type T
- if
[] |- e :: T
, - then there exists a value
v
such that[] ; e ==> v
.
How do we prove theorems about languages?
By induction.
Mathematical induction in PL
1. Induction on natural numbers
To prove ∀n.P(n) we need to prove:
- Base case: P(0)
- Inductive case: P(n + 1) assuming the induction hypothesis (IH): that P(n) holds
Compare with inductive definition for natural numbers:
data Nat = Zero -- base case
| Succ Nat -- inductive case
No reason why this would only work for natural numbers…
In fact we can do induction on any inductively defined mathematical object (= any datatype)!
- lists
- trees
- programs!!!
2. Induction on programs
e ::= n
| x
| e1 + e2
| \x -> e
| e1 e2
To prove ∀e.P(e) we need to prove:
- Base case 1:
P(n)
- Base case 2:
P(x)
- Inductive case 1:
P(e1 + e2)
assuming the IH: thatP(e1)
andP(e2)
hold - Inductive case 2:
P(\x -> e)
assuming the IH: thatP(e)
holds - Inductive case 3:
P(e1 e2)
assuming the IH: thatP(e1)
andP(e2)
hold
Proof: Take 1
Theorem For any program e
and type T
- if
[] |- e :: T
, - then there exists a value
v
such that[] ; e ==> v
.
Proof:
Base case 1 (n
): By E-Num
we have [] ; n ==> n
, hence v == n
.
…
Inductive case 3 (e1 e2
): Assuming that [] |- e1 e2 :: T
, prove that [] ; e1 e2 ==> v
. We need to prove that:
[] ; e1 ==> <E, x, e>
[] ; e2 ==> v2
[x:=v2] ; e ==> v
- follows by IH, but 1 and 3 do not. We need to generalize the theorem to make the induction go through!
Generalizing the Theorem
Intuitively, we need to change our theorem in three ways:
- Generalize to arbitrary
G
andE
- Prove that the resulting value
v
has typeT
- Prove all closures we create terminate, when given appropriate arguments
Let’s define what it means for a value to be “well-typed and terminating”!
Well-Behaved Values
Let’s define a new relation: v :: T
(value v
is well-behaved at type T
)
- Intuitive meaning:
v
has typeT
and also terminates on all well-behaved arguments (if it’s a closure).
[V-Num] --------
n :: Int
forall v1 :: T1 .
(x:=v1,E) ; e ==> v2 v2 :: T2
[V-Clos] -------------------------------
<E, x, e> :: T1 -> T2
We extend this relation to environments: E :: G
(environment E
is well-behaved in context G
)
- Intuitive meaning:
G
andE
have the same variables, and each value inE
is well-behaved at itsG
-type
[E-Nil] --------
[] :: []
v :: T E :: G
[E-Bnd] ---------------------
(x:=v, E) :: (x:T, G)
Main Lemma
Now we can state our generalized theorem:
Lemma: For any program e
, type T
, environment E
, context G
:
- If
G |- e :: T
- and
E :: G
then there exists a value v
such that
E ; e ==> v
- and
v :: T
.
Proof:
Base case 1 (n
):
Because G |- n :: T
, then T
is Int
by T-Num
. With v == n
: (A) E ; n ==> n
by E-Num
and (B) n :: Int
by V-Num
.
Base case 2 (x
):
Because G |- x :: T
, we know that G = (x:T,...)
by T-Var
. Hence, from (2) and E-Bnd
we have E = (x:=v, ...)
and v :: T
. Hence we get: (A) E ; x ==> v
by E-Var
and (B) v :: T
.
Inductive case 1 (e1 + e2
):
Because G |- e1 + e2 :: T
, then by T-Add
, T
is Int
and also (3) G |- e1 :: Int
and (4) G |- e2 :: Int
. By IH from (3) we get (5) E ; e1 ==> v1
and v1 :: Int
, hence by V-Num
v1
is some numeral n1
. Similarly from (4) we get (6) E ; e2 ==> n2
. With n = n1 + n2
, we get (A) E ; (e1 + e2) ==> n
by E-Add
, and (B) n :: Int
by V-Num
.
Inductive case 2 (\x -> e
):
Because G |- \x -> e :: T
, then by T-Lam
, T
is T1 -> T2
and also (3) x:T1, G |- e :: T2
. Now pick an arbitrary v1
such that v1 :: T1
. Then x:=v1,E :: x:T1,G
by E-Bnd
and (2). Hence using IH on (3) we get (4) (x:=v1,E) ; e ==> v2
and v2 :: T2
. With v = <E,x,e>
we get (A) E ; \x -> e ==> v
and (B) v :: T1 -> T2
by V-Clos
and (4).
Inductive case 3 (e1 e2
):
Because G |- e1 e2 :: T
, then by T-App
we get (3) G |- e1 :: T' -> T
and (4) G |- e2 :: T'
. By IH from (4) we get (5) E ; e2 ==> v2
and (6) v2 :: T'
. By IH from (3) we get (7) E ; e1 ==> v1
and (8) v1 :: T' -> T
, hence by V-Clos
: v1
is a closure <E',x,e>
and moreover given (6), we also have (9) (x:=v2,E) ; e ==> v
and (10) v :: T
. By E-App
from (7), (5), (9) we have (A) E ; (e1 e2) ==> v
and (B) follows by (10).
Now to the Theorem
Theorem For any program e
and type T
- if
[] |- e :: T
, - then there exists a value
v
such that[] ; e ==> v
.
Proof: Because [] :: []
by E-Nil
, we can invoke Lemma with G = []
, E = []
to get v
such that [] ; e ==> v
.
That’s all folks