Simply-Typed Lambda Calculus (Slides made by Hongjin Liang, mostly following Dan Grossman's teaching materials)
Simply-Typed Lambda Calculus (Slides made by Hongjin Liang, mostly following Dan Grossman’s teaching materials)
Review of untyped A-calculus Syntax:notation for defining functions (Terms)M,N :x Ax.MM N Semantics:reduction rules (x.M)N→M[W/x B) M→M' N-N' M→M' MN→M'N MN→MN' λx.M→λX.M
Review of untyped -calculus • Syntax: notation for defining functions (Terms) M, N ::= x | x. M | M N • Semantics: reduction rules λ𝑥. 𝑀 𝑁 → 𝑀[𝑁/𝑥] () 𝑀 → 𝑀′ 𝑀 𝑁 → 𝑀′𝑁 𝑀 → 𝑀′ λ𝑥. 𝑀 → λ𝑥. 𝑀′ 𝑁 → 𝑁′ 𝑀 𝑁 → 𝑀 𝑁′
x.M0N-→M[N/x] (β) M→M' (f.入z.f(fz)(y.y+x) MN→M'N →入z.(y.y+x)(y.y+x)z) N→N' MN→MN' -→入z.(y.y+x)(z+x) M→M' >入z.Z+X+X λX.M→λX.M
(f. z. f (f z)) (y. y+x) → z. (y. y+x) ((y. y+x) z) → z. (y. y+x) (z+x) → z. z+x+x λ𝑥. 𝑀 𝑁 → 𝑀[𝑁/𝑥] () 𝑀 → 𝑀′ 𝑀 𝑁 → 𝑀′𝑁 𝑀 → 𝑀′ λ𝑥. 𝑀 → λ𝑥. 𝑀′ 𝑁 → 𝑁′ 𝑀 𝑁 → 𝑀 𝑁′
Review of untyped A-calculus (Ax.Xx)(7X.xx) >(2x.xx)(x.×x) 〉… This class:adding a type system (We will see that well-typed terms in STLC always terminate.)
Review of untyped -calculus (x. x x) (x. x x) → (x. x x) (x. x x) → … This class: adding a type system (We will see that well-typed terms in STLC always terminate.)
Why types Type checking catches "simple"mistakes early ·Example:2+true+“a” .(Type safety)Well-typed programs will not go wrong Ensure execution never reach a "meaningless"state But"meaningless"depends on the semantics(each language typically defines some as type errors and others run-time errors) Typed programs are easier to analyze and optimize Compilers can generate better code (e.g.access components of structures by known offset) Cons:impose constraints on the programmer Some valid programs might be rejected
Why types • Type checking catches “simple” mistakes early • Example: 2 + true + “a” • (Type safety) Well-typed programs will not go wrong • Ensure execution never reach a “meaningless” state • But “meaningless” depends on the semantics (each language typically defines some as type errors and others run-time errors) • Typed programs are easier to analyze and optimize • Compilers can generate better code (e.g. access components of structures by known offset) Cons: impose constraints on the programmer • Some valid programs might be rejected
Why formal type systems Many typed languages have informal descriptions of the type systems (e.g.,in language reference manuals) A fair amount of careful analysis is required to avoid false claims of type safety A formal presentation of a type system is a precise specification of the type checker And allows formal proofs of type safety
Why formal type systems • Many typed languages have informal descriptions of the type systems (e.g., in language reference manuals) • A fair amount of careful analysis is required to avoid false claims of type safety • A formal presentation of a type system is a precise specification of the type checker • And allows formal proofs of type safety
What we will study about types ·Type system Typing rules:assign types to terms Type safety(soundness of typing rules):well-typed terms cannot go wrong Connection to constructive propositional logic ·Curry-Howard isomorphism:“Propositions are Types'”, “Proofs are Programs
What we will study about types • Type system • Typing rules: assign types to terms • Type safety (soundness of typing rules): well-typed terms cannot go wrong • Connection to constructive propositional logic • Curry-Howard isomorphism: “Propositions are Types”, “Proofs are Programs
Simply-typed A-calculus(STLC) base type (e.g.int,bool) function type (Types)t,o=T|o→t An infinite number of types: int-→int,int→(int→int),(int->int)>int, →is right-associative:t→t→tist→(t→t)
Simply-typed -calculus (STLC) (Types) , ::= T | → base type (e.g. int, bool) function type An infinite number of types: int → int, int → (int → int), (int → int) → int, … → is right-associative: → → is → ( → )
Simply-typed A-calculus(STLC) (Types)t,o=T|o→t (Terms)M,N ::xx t.M MN
Simply-typed -calculus (STLC) (Terms) M, N ::= x | x : . M | M N (Types) , ::= T | →
Reduction rules (x:t.M)N→M[N/x] (β) M→M' MN→M'N Same as untyped A-calculus N→N' MN→MN' M→M' X:t.M→λx:t.M1
Reduction rules λ𝑥: 𝜏. 𝑀 𝑁 → 𝑀[𝑁/𝑥] 𝑀 → 𝑀′ 𝑀 𝑁 → 𝑀′𝑁 𝑀 → 𝑀′ λ𝑥: 𝜏. 𝑀 → λ𝑥: 𝜏. 𝑀′ 𝑁 → 𝑁′ 𝑀 𝑁 → 𝑀 𝑁′ Same as untyped -calculus ()