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