Principles of Programming Languages

Type Systems

Andrei Arusoaie1
1 Department of Computer Science
Outline

Motivation
Outline

Motivation

Typing
Outline

Motivation

Typing

Typing rules
Outline

Motivation

Typing

Typing rules

Properties
Static type checking

▶ Type systems are essential in programming languages

▶ Most languages have values categorised in certain types
▶ Static type systems perform compile-time type checking
▶ Type checkers verify that operations are applied to values
of appropriate types
▶ Type safety: A well-typed program cannot produce type
errors at runtime
▶ Lean 4 is a dependently-typed proof assistant with a strong
static type system
Motivation

Type errors in Lean 4:

-- Lean 4 type error example

#check true + false
-- application type mismatch
-- true + false
-- argument
-- true
-- has type
-- Bool : Type
-- but is expected to have a numeric type
Motivation

... but in Javascript:

// Welcome to [Link] v18.16.0.

// Type ".help" for more information.
> true + false
1
> 2 + '4'
'24'
> '2' + 4
'24'
> 2 * '4'
8
> '2' * 4
8
Motivation

What is the result type of && in Javascript?

// Welcome to [Link] v18.16.0.
// Type ".help" for more information.
> 0 && true
0
> true && 0
0
> 0 && false
0
> false && 0
false
Motivation

Confusing outputs in Javascript:

// Welcome to [Link] v18.16.0.
// Type ".help" for more information.
> false == []
true
> false == ![]
true
> [] == ![]
true
Strongly vs. Weakly typed languages

▶ Lean 4 is an example of a strongly-typed language

▶ Javascript is an example of a weakly-typed language
Strongly vs. Weakly typed languages

▶ Lean 4 is an example of a strongly-typed language

▶ Javascript is an example of a weakly-typed language
▶ Strongly-typed languages: type safety, readability,
performance vs. less flexibility, steep learning curve
Strongly vs. Weakly typed languages

▶ Lean 4 is an example of a strongly-typed language

▶ Javascript is an example of a weakly-typed language
▶ Strongly-typed languages: type safety, readability,
performance vs. less flexibility, steep learning curve
▶ Weakly-typed languages: flexibility, easy to learn, less
verbose code vs. runtime errors, no type safety, possible
less performance, debugging troubles
Goal for this lecture

Our goal in this lecture is to understand how to define a type

system and what are its desired properties.
Steps:
▶ We first mix the arithmetic and boolean expressions
▶ We define the small-step SOS for such expressions
▶ We define a type system for these expressions
▶ We formulate and prove the following properties for our
type system: progress, preservation, soundness
Abstract Syntax

▶ We define a unified expression type combining arithmetic

and boolean expressions
▶ Inductive types define syntax compositionally through
constructors
▶ This allows mixing expressions of different types
(potentially causing type errors)
▶ Coercions can be used to make certain types implicitly
convertible
▶ Notation provides syntactic sugar for better readability
Mixing boolean and arithmetic expressions
inductive Exp where
| anum : Int -> Exp
| avar : String -> Exp
| aplus : Exp -> Exp -> Exp
| amult : Exp -> Exp -> Exp
| btrue : Exp
| bfalse : Exp
| bnot : Exp -> Exp
| band : Exp -> Exp -> Exp
| blessthan : Exp -> Exp -> Exp
deriving Repr

open Exp

instance : OfNat Exp n where

ofNat := anum n
instance : Coe String Exp where
coe := avar

infixl:50 " +' " => aplus

infixl:40 " *' " => amult
infixl:60 " <' " => blessthan
infixl:75 " &&' " => band
Remember: Small-step SOS

▶ Small-step semantics defines how expressions reduce one

step at a time
▶ An environment (Env) maps variables to their values
sigma
▶ Evaluation relation e1 −−−→ e2 means expression e1
reduces to e2 in environment sigma
▶ Evaluation proceeds by pattern matching on expression
structure
▶ Reduction rules specify how to evaluate each syntactic
construct
▶ Some expressions may get stuck if they are ill-typed
Small-Step SOS for mixed expressions

abbrev Env := String -> Nat

inductive eval : Exp -> Env -> Exp -> Prop where
| const : forall i sigma,
eval (anum i) sigma (anum i)
| lookup : forall x sigma,
eval (avar x) sigma (anum (sigma x))
| add_l : forall a1 a2 sigma a1',
eval a1 sigma a1' ->
eval (a1 +' a2) sigma (a1' +' a2)
| add_r : forall a1 a2 sigma a2',
eval a2 sigma a2' ->
eval (a1 +' a2) sigma (a1 +' a2')
| add : forall i1 i2 sigma n,
n = i1 + i2 ->
eval (anum i1 +' anum i2) sigma (anum n)
-- ... (similar rules for mult, lessthan, not, band)

open eval
notation:98 A " -[ " S " ]-> " B => eval A S B
Remember: reflexive-transitive closure

▶ The reflexive-transitive closure represents zero or more

evaluation steps
▶ Reflexivity: Every expression can take zero steps to itself
▶ Transitivity: If e1 → e2 and e2 →∗ e3 , then e1 →∗ e3
▶ This captures multi-step evaluation from an expression to
its final result
▶ Well-typed expressions evaluate to values
▶ Ill-typed expressions may get stuck during evaluation
Well-typed expressions

inductive eval_closure : Exp -> Env -> Exp -> Prop where
| refl : forall e sigma,
eval_closure e sigma e
| tran : forall e1 e2 e3 sigma,
eval e1 sigma e2 ->
eval_closure e2 sigma e3 ->
eval_closure e1 sigma e3
open eval_closure
notation:99 A " -[ " S " ]>* " B => eval_closure A S B

def Env0 : Env := fun _ => 0

example : (2 +' "n") -[ Env0 ]>* 2 := by

apply tran (e2 := 2 +' 0)
· apply add_r
apply lookup
· apply tran
· apply add
rfl
· apply refl

▶ Note: the expression 2 +' "n" is evaluated to a value.

Ill-typed expressions

▶ It is impossible to obtain a value for ill-typed expressions

using eval
▶ In such cases we say that 2 +’ btrue is stuck:
2 +’ btrue does not evaluate to a value and no
transitions via eval are possible from it
▶ Terms that are not values and cannot be reduced to values
are stuck
▶ How do we detect stuck terms? Define a type system to
exclude nonsensical terms
A type system for expressions

▶ Our expressions include both numbers and boolean values

▶ To exclude terms we don’t want to have meaning (e.g., 2 +’
btrue), we define a typing relation
▶ The typing relation relates terms to the types of their final
(evaluated) results
▶ Types classify expressions into categories (e.g., Nat, Bool)
▶ The typing relation e : T means expression e has type T
▶ Type checking verifies that expressions satisfy typing rules
Adding types

▶ Types: Bool and Nat

▶ Lean 4:
inductive Typ where
| Nat : Typ
| Bool : Typ
deriving Repr, DecidableEq
open Typ
▶ We define a relation :⊆ Exp × Typ using inference rules for
typing
▶ When e : Nat we say that the type of e is Nat
▶ Checking whether an expression has a certain type
reduces to finding a derivation (proof) using the typing
rules
Typing rules - I

n∈N
anum n : Nat TNUM

x ∈ Var
avar x : Nat TVAR

a1 : Nat a2 : Nat
TPLUS
a1 +′ a2 : Nat

a1 : Nat a2 : Nat
TMUL
a1 ∗′ a2 : Nat
Typing rules - example

2∈N x ∈ Var
TNUM
2 : Nat x : Nat TVAR
TPLUS
2 +′ x : Nat
Typing rules - II

·
TTRUE
btrue : Bool

·
TFALSE
bfalse : Bool

b : Bool
TNOT
bnot b : Bool

b1 : Bool b2 : Bool
TAND
band b1 b2 : Bool

a1 : Nat a2 : Nat
TLT
a1 <′ a2 : Bool
Typing rules - example

2∈N x ∈ Var
TNUM
2 : Nat x : Nat TVAR
′ TLEQ
2 < x : Bool
Typing derivations

▶ Typing derivations are proof trees showing that

expressions are well-typed
▶ Each node in the tree corresponds to a typing rule
application
▶ inductive in Lean 4 naturally encode typing rules
▶ Type derivation proofs demonstrate that an expression has
a particular type
▶ Typing rules are syntax-directed: each expression form
has a specific rule
▶ Typing derivations are different from evaluating
expressions!!
Typing rules - I - in Lean 4

inductive type_of : Exp -> Typ -> Prop where

| t_num : forall n,
type_of (anum n) Nat
| t_var : forall x,
type_of (avar x) Nat
| t_plus : forall a1 a2,
type_of a1 Nat ->
type_of a2 Nat ->
type_of (a1 +' a2) Nat
| t_mult : forall a1 a2,
type_of a1 Nat ->
type_of a2 Nat ->
type_of (a1 *' a2) Nat
-- ...
Typing rules - II - in Lean 4
inductive type_of : Exp -> Typ -> Prop where
-- ...
| t_true :
type_of btrue Bool
| t_false :
type_of bfalse Bool
| t_not : forall b,
type_of b Bool ->
type_of (bnot b) Bool
| t_and : forall b1 b2,
type_of b1 Bool ->
type_of b2 Bool ->
type_of (band b1 b2) Bool
| t_lessthan : forall a1 a2,
type_of a1 Nat ->
type_of a2 Nat ->
type_of (blessthan a1 a2) Bool
Values and canonical forms

▶ Terms that cannot be reduced anymore are said to be in a

normal form
▶ Values are fully evaluated expressions that cannot be
reduced further
▶ For natural numbers: the value is anum n for some n ∈ N
▶ For booleans: the values are btrue and bfalse
▶ Canonical forms lemma: If an expression is both a value
and well-typed, it must have a specific form
▶ If e is a value and e : Bool, then e is either btrue or
bfalse
▶ These lemmas are crucial for proving type safety
properties
Values

inductive nat_value : Exp -> Prop where

| n_val : forall n, nat_value (anum n)

inductive bool_value : Exp -> Prop where

| b_true : bool_value btrue
| b_false : bool_value bfalse

def value (e : Exp) : Prop :=

nat_value e \/ bool_value e
Canonical forms

theorem bool_canonical :
forall e,
type_of e Bool ->
value e ->
bool_value e := by ...

theorem nat_canonical :
forall e,
type_of e Nat ->
value e ->
nat_value e := by ...
Progress

▶ Progress captures the fact that well-typed expressions

make progress
▶ Progress: A well-typed expression is either a value or can
take a step
▶ Formally: If ⊢ e : T , then either e is a value or ∃e′ such that
e → e′
▶ Progress guarantees that well-typed programs never get
stuck
▶ This is half of type safety: well-typed programs don’t
encounter runtime type errors
▶ Proof typically proceeds by induction on the typing
derivation
▶ Each case corresponds to a typing rule
Progress theorem

theorem progress :
forall e T sigma,
type_of e T ->
(value e \/ exists e', e -[ sigma ]-> e') :=
by sorry
Type preservation

▶ Type preservation (Subject Reduction) is critical for type

safety
▶ It says: if a well-typed expression is reduced in one step,
the result is also well-typed
▶ Formally: If ⊢ e : T and e → e′ , then ⊢ e′ : T
▶ Preservation ensures that evaluation preserves types
▶ This is the other half of type safety
▶ Together with progress, preservation implies that
well-typed programs can only produce well-typed results
▶ Proof typically by induction on the typing derivation
Type preservation theorem

theorem preservation :
forall e e' T sigma,
type_of e T ->
(e -[ sigma ]-> e') ->
type_of e' T :=
by sorry
Type soundness

▶ Type Soundness: “Well-typed programs don’t go wrong”

▶ Combines progress and preservation for multi-step
evaluation
▶ If ⊢ e : T and e →∗ e′ , then either e′ is a value or ∃e′′ such
that e′ → e′′
▶ Soundness theorem is a corollary of progress and
preservation
▶ Proof by induction on the reflexive-transitive closure
▶ This is the fundamental safety guarantee of the type
system
▶ Well-typed programs never get stuck during execution
▶ A well-typed expression cannot reach a stuck state
Type soundness theorem

theorem soundness :
forall e e' T sigma,
type_of e T ->
(e -[ sigma ]>* e') ->
(value e' \/ exists e'', e' -[ sigma ]-> e'') :=

The implications of type soundness are very strong: if a

program can be proved to be well-typed, then it is guaranteed
not to produce erroneous results.