/* Semantic colors */
--text-color: var(--foreground);
--heading-color: var(--purple);
--link-color: var(--cyan);
--link-hover: var(--pink);
--code-bg: var(--current-line);
--code-border: #6272a4;
--toc-bg: #21222c;
--toc-border: var(--current-line);
--blockquote-border: var(--purple);
--table-border: var(--current-line);
}
* {
box-sizing: border-box;
}
body {
font-family: Georgia, 'Times New Roman', serif;
line-height: 1.7;
max-width: 1400px;
margin: 0 auto;
padding: 20px;
background-color: var(--bg-color);
color: var(--text-color);
display: flex;
gap: 2rem;
}
/* Table of Contents */
#TOC {
position: sticky;
top: 20px;
min-width: 250px;
max-width: 300px;
height: fit-content;
max-height: calc(100vh - 40px);
overflow-y: auto;
background-color: var(--toc-bg);
border: 1px solid var(--toc-border);
border-radius: 8px;
padding: 1.5rem;
font-size: 0.9rem;
}
#TOC ul {
list-style: none;
padding-left: 0;
margin: 0;
}
#TOC > ul > li {
margin-bottom: 0.5rem;
}
#TOC ul ul {
padding-left: 1rem;
margin-top: 0.3rem;
}
#TOC a {
color: var(--link-color);
text-decoration: none;
display: block;
padding: 0.2rem 0;
transition: all 0.2s;
}
#TOC a:hover {
color: var(--link-hover);
transform: translateX(4px);
}
/* Main content */
main {
flex: 1;
min-width: 0;
max-width: 800px;
}
h1, h2, h3, h4, h5, h6 {
color: var(--heading-color);
margin-top: 2rem;
margin-bottom: 1rem;
line-height: 1.3;
font-weight: 600;
}
h1 {
font-size: 2.5rem;
border-bottom: 2px solid var(--purple);
padding-bottom: 0.5rem;
color: var(--pink);
}
h2 {
font-size: 2rem;
border-bottom: 1px solid var(--current-line);
padding-bottom: 0.3rem;
}
h3 { font-size: 1.5rem; color: var(--cyan); }
h4 { font-size: 1.25rem; color: var(--green); }
h5 { font-size: 1.1rem; color: var(--orange); }
h6 { font-size: 1rem; color: var(--yellow); }
a {
color: var(--link-color);
text-decoration: none;
transition: color 0.2s;
}
a:hover {
color: var(--link-hover);
text-decoration: underline;
}
/* Code blocks */
pre {
background-color: var(--code-bg);
border: 1px solid var(--code-border);
border-radius: 6px;
padding: 1rem;
overflow-x: auto;
font-size: 0.9rem;
}
code {
font-family: 'Consolas', 'Monaco', 'Courier New', monospace;
background-color: var(--code-bg);
padding: 0.2rem 0.4rem;
border-radius: 3px;
font-size: 0.9em;
color: var(--pink);
}
pre code {
background-color: transparent;
padding: 0;
color: var(--foreground);
}
/* Blockquotes */
blockquote {
margin: 1.5rem 0;
padding: 1rem;
padding-left: 1.5rem;
border-left: 4px solid var(--blockquote-border);
background-color: rgba(189, 147, 249, 0.1);
color: var(--foreground);
font-style: italic;
border-radius: 0 6px 6px 0;
}
blockquote p {
margin: 0.5rem 0;
}
/* Tables */
table {
border-collapse: collapse;
width: 100%;
margin: 1.5rem 0;
}
table th,
table td {
border: 1px solid var(--table-border);
padding: 0.75rem;
text-align: left;
}
table th {
background-color: var(--code-bg);
color: var(--purple);
font-weight: bold;
}
table tr:nth-child(even) {
background-color: rgba(68, 71, 90, 0.3);
}
table tr:hover {
background-color: rgba(68, 71, 90, 0.5);
}
/* Images */
img {
max-width: 100%;
height: auto;
border-radius: 6px;
border: 1px solid var(--current-line);
}
/* Lists */
ul, ol {
margin: 1rem 0;
padding-left: 2rem;
}
li {
margin: 0.5rem 0;
}
li::marker {
color: var(--purple);
}
/* Horizontal rule */
hr {
border: none;
border-top: 2px solid var(--current-line);
margin: 2rem 0;
}
/* Inline emphasis */
strong {
color: var(--orange);
font-weight: bold;
}
em {
color: var(--yellow);
font-style: italic;
}
/* Selection */
::selection {
background-color: var(--selection);
color: var(--foreground);
}
/* Responsive design */
@media (max-width: 900px) {
body {
flex-direction: column;
}
#TOC {
position: static;
max-width: 100%;
max-height: 300px;
margin-bottom: 2rem;
}
main {
max-width: 100%;
}
}
/* Scrollbar styling */
::-webkit-scrollbar {
width: 12px;
}
::-webkit-scrollbar-track {
background: var(--bg-color);
}
::-webkit-scrollbar-thumb {
background: var(--current-line);
border-radius: 6px;
}
::-webkit-scrollbar-thumb:hover {
background: var(--comment);
}
/* Title block */
#title-block-header {
margin-bottom: 3rem;
padding-bottom: 1rem;
border-bottom: 2px solid var(--purple);
}
#title-block-header .title {
margin-top: 0;
color: var(--pink);
}
#title-block-header .subtitle {
color: var(--purple);
font-size: 1.3rem;
margin: 0.5rem 0;
}
#title-block-header .author {
color: var(--cyan);
margin: 0.3rem 0;
}
#title-block-header .date {
color: var(--comment);
font-size: 0.9rem;
margin: 0.3rem 0;
}
- Chapter 1 Introduction to Type Theory
- Chapter 2 Mathematical Foundations: Set Theory and Algebra
- Chapter 3 Category Theory and Types
- Chapter 4 Combinatory Logic and the Foundations of Typing
- Chapter 5 Lambda Calculus and Typed Lambda Calculi
- Chapter 6 Subtyping and Record Types
- Chapter 7 Parametric Polymorphism: System F and Beyond
- Chapter 8 Dependent Types and the Calculus of Constructions
- Chapter 9 Curry–Howard Correspondence: Logic as Types
- Chapter 10 Semantic Analysis and Type-Checking Algorithms
- Chapter 11 Lattice Theory in Type Systems and Abstract Interpretation
- Chapter 12 Type Systems in Functional Programming Languages
- Chapter 13 Type Systems in Object-Oriented, Logic-Oriented & Imperative Languages
- Chapter 14 Type Inference, Gradual Typing and Future Directions
In this chapter we introduce the fundamental ideas of type theory. We begin with the informal notion of a “type,” survey its historical roots and modern motivations, then present the basic judgmental framework (terms, contexts, typing rules) common to virtually every typed formalism. Finally, we fix notational and metatheoretic conventions that will guide the rest of the book.
- 1 What Is a “Type”? History and Motivation
1.1.1 Informal notion
A “type” is, at heart, a classification of computational or mathematical
objects that constrains how they may be combined. In programming, types
prevent meaningless operations (e.g. adding a Boolean to an integer),
document programmer intent, and enable compiler optimizations. In logic,
types correspond to propositions—proof‐terms inhabit types. In
mathematics, types can model sets, categories, or algebraic
structures.
1.1.2 Early origins
• Bertrand Russell’s Theory of Types (1908) sought to avoid
paradoxes in set theory by stratifying sets into “types.”
• Alonzo Church (1940s) introduced the simply typed λ‐calculus, adding a
layer of types to the untyped λ‐calculus.
• Haskell Curry and Robert Feys developed Combinatory
Logic, which implicitly carries type discipline.
• In the 1970s, Robin Milner’s Hindley–Milner system formalized
polymorphic type inference, underpinning ML and Haskell.
1.1.3 Modern motivations
1. Safety: Types rule out whole classes of runtime errors (ill‐formed
memory accesses, mismatched data).
2. Abstraction: Interfaces expressed via types decouple modules and
allow separate compilation.
3. Documentation: A type signature is a concise specification.
4. Optimization: Knowing types lets compilers generate more efficient
code.
5. Verification: Dependent types allow expressing and machine‐checking
rich correctness properties.
- 2 Basic Concepts: Terms, Judgments, Typing Rules
1.2.1 Syntax of Terms and Types
We start with the simply typed λ‐calculus (STLC) as our running
example. Let metavariables
–
x,y,zx,y,z
range over term variables
–
τ,σ\tau,\sigma
range over types
–
M,NM,N
range over terms
Types
τ\tau
are given by the grammar
τ::=𝐁𝐨𝐨𝐥∣𝐍𝐚𝐭∣τ1→τ2
\tau ::= \mathbf{Bool}
\mid \mathbf{Nat}
\mid \tau_1 \to \tau_2
Terms
MM
by
M::=x∣λx:τ.M∣M1M2∣𝐭𝐫𝐮𝐞∣𝐟𝐚𝐥𝐬𝐞∣0∣succ(M)
M ::= x
\mid \lambda x:\tau.\;M
\mid M_1\;M_2
\mid \mathbf{true}\mid \mathbf{false}
\mid 0\mid\mathrm{succ}(M)
1.2.2 Typing contexts and judgments
A context
Γ\Gamma
is a finite mapping from term variables to types, e.g.
Γ={x:τ1,y:τ2,…}.
\Gamma = \{\,x:\tau_1,\;y:\tau_2,\;\dots\}.
A typing judgment has the form
Γ⊢M:τ
\Gamma\;\vdash\;M:\tau
and asserts “under assumptions in
Γ\Gamma,
term
MM
has type
τ\tau.”
1.2.3 Inference rules
We present several standard rules in natural deduction
style.
(Var)
$$
\infer[\textsc{Var}]
{\Gamma\vdash x:\tau}
{x:\tau\in\Gamma}
$$
(Abs)
$$
\infer[\textsc{Abs}]
{\Gamma\vdash \lambda x:\tau_1.\;M:\;\tau_1\to\tau_2}
{\Gamma,x:\tau_1\;\vdash M:\tau_2}
$$
(App)
$$
\infer[\textsc{App}]
{\Gamma\vdash M\,N:\tau_2}
{\Gamma\vdash M:\tau_1\to\tau_2
\quad
\Gamma\vdash N:\tau_1}
$$
(Bool‐True)
$$
\infer[\textsc{True}]
{\Gamma\vdash \mathbf{true}:\mathbf{Bool}}
{\,}
$$
(Nat‐Succ)
$$
\infer[\textsc{Succ}]
{\Gamma\vdash \mathrm{succ}(M):\mathbf{Nat}}
{\Gamma\vdash M:\mathbf{Nat}}
$$
These rules specify exactly which term‐type combinations are well‐formed.
1.2.4 Example: ill‐typed term
Consider the untyped λ‐term
Ω=(λx.xx)(λx.xx).
\Omega = (\lambda x.\;x\;x)\;(\lambda x.\;x\;x).
In STLC this term is untypable: attempting to assign
x:τ→τx:\tau\to\tau
forces
τ→τ=τ\tau\to\tau=\tau,
no solution in the simply typed world. Thus ill‐typed programs
are rejected at compile time.
- 3 Notation, Metatheory and Conventions
1.3.1 Binding, α‐equivalence, substitution
– We write
λx.M\lambda x.\,M
for abstraction;
xx
binds free occurrences in
MM.
–
M≡αNM\equiv_\alpha N
denotes equality up to renaming of bound variables.
– Capture‐avoiding substitution is written
M[N/x]M[N/x],
replacing free
xx
in
MM
by
NN.
1.3.2 Context operations
–
Γ,x:τ\Gamma,x:\tau
extends
Γ\Gamma
with a fresh binding.
– We assume weakening and exchange admissible: if
Γ⊢M:τ\Gamma\vdash M:\tau,
adding irrelevant bindings or permuting order does not invalidate
it.
1.3.3 Metatheoretic properties
Two properties are central in typed λ‐calculi:
(Progress)
If
⌀⊢M:τ\varnothing\vdash M:\tau,
then either
MM
is a value or there exists
M′M'
with
M→M′M\to M'.
(Preservation) (a.k.a. “Subject Reduction”)
If
Γ⊢M:τ\Gamma\vdash M:\tau
and
M→M′M\to M',
then
Γ⊢M′:τ\Gamma\vdash M':\tau.
Together, these yield type safety: well-typed programs do not go wrong.
1.3.4 Programming‐language example
Below is a tiny OCaml‐style AST and type-checker fragment for Booleans
and natural numbers:
type ty = Bool | Nat | Arrow of ty * ty
type term =
| Var of string
| Abs of string * ty * term
| App of term * term
| True | False
| Zero | Succ of term
exception TypeError of string
let rec lookup x ctx =
try List.assoc x ctx
with Not_found -> raise (TypeError ("Unbound var " ^ x))
let rec tc ctx = function
| Var x -> lookup x ctx
| Abs(x, t1, m) ->
let t2 = tc ((x,t1)::ctx) m in
Arrow(t1, t2)
| App(m,n) ->
(match tc ctx m with
| Arrow(t11,t12) ->
let t2 = tc ctx n in
if t11 = t2 then t12
else raise (TypeError "Arg type mismatch")
| _ -> raise (TypeError "Expected function"))
| True | False -> Bool
| Zero -> Nat
| Succ m ->
if tc ctx m = Nat then Nat
else raise (TypeError "succ expects Nat")This checker follows exactly the rules of section 1.2.3.
1.3.5 Chapter summary and road‐map
We have seen:
– The idea of types as classifications ensuring safety and
expressivity.
– The formal machinery of contexts, judgments, and inference
rules.
– Notational conventions (binding, substitution, α–equivalence).
– Metatheoretic goals: progress & preservation.
In Chapter 2 we anchor these ideas in classical mathematical structures—sets, relations and algebraic models—and show how types arise from familiar constructions in set theory and universal algebra.
- –
In this chapter we review the classical mathematical notions of sets, relations and functions, then introduce the algebraic‐structure concepts (monoids, lattices, universal algebras) that underlie many type‐theoretic constructions. Finally, we show how data types in programming languages correspond to set‐ and algebraic‐theoretic constructs.
1 Sets, Relations and Functions
1.1 Sets and Set‐Operations
A set AA is an unordered collection of distinct elements. We write x∈Ax\in A to mean “xx is a member of AA,” and A⊆BA\subseteq B to mean “every element of AA is also in BB.”
Standard operations on sets A,BA,B: A∪B={x∣x∈A or x∈B},A∩B={x∣x∈A and x∈B}, A\cup B = \{\,x \mid x\in A \text{ or } x\in B\}, \quad A\cap B = \{\,x \mid x\in A \text{ and } x\in B\}, A\B={x∣x∈A and x∉B},𝒫(A)={X∣X⊆A}. A\setminus B = \{\,x \mid x\in A \text{ and } x\notin B\}, \quad \mathcal P(A) = \{\,X \mid X\subseteq A\}. The cardinality |A||A| of a finite set AA is the number of its elements. For infinite sets one distinguishes countable vs. uncountable, but in type theory we often treat all sets extensionally.
- 1.2 Relations
A binary relation RR between AA and BB is a subset R⊆A×B. R \;\subseteq\; A\times B. We write aRba\,R\,b as shorthand for (a,b)∈R(a,b)\in R. Important special cases:
– Domain
dom(R)={a∣∃b.aRb}\mathrm{dom}(R)=\{\,a\mid \exists b.\;a\,R\,b\}.
– Range
ran(R)={b∣∃a.aRb}\mathrm{ran}(R)=\{\,b\mid \exists a.\;a\,R\,b\}.
Given relations R⊆A×BR\subseteq A\times B and S⊆B×CS\subseteq B\times C, their composition is S∘R={(a,c)∣∃b.aRb∧bSc}⊆A×C. S\circ R \;=\; \{\,(a,c)\mid \exists b.\;a\,R\,b \,\wedge\, b\,S\,c\}\;\subseteq\;A\times C. The inverse or converse of RR is R−1={(b,a)∣(a,b)∈R}⊆B×A. R^{-1} \;=\;\{(b,a)\mid (a,b)\in R\}\;\subseteq\;B\times A.
Key relation properties on AA (R⊆A×AR\subseteq A\times A):
• Reflexive:
∀a∈A.aRa\forall a\in A.\;a\,R\,a.
• Symmetric:
∀a,b.aRb⟹bRa\forall a,b.\;a\,R\,b\implies b\,R\,a.
• Transitive:
∀a,b,c.(aRb∧bRc)⟹aRc\forall a,b,c.\;(a\,R\,b\wedge b\,R\,c)\implies a\,R\,c.
An equivalence relation is reflexive, symmetric and transitive; it partitions AA into equivalence classes. A partial order is reflexive, antisymmetric (aRb∧bRa⟹a=ba\,R\,b\wedge b\,R\,a\implies a=b) and transitive.
- 1.3 Functions
A function f:A→Bf\colon A\to B is a relation that is both ∀a∈A.∃!b∈B.(a,b)∈f. \forall a\in A.\;\exists!\;b\in B.\;(a,b)\in f. Equivalently, ff is a mapping a↦f(a)a\mapsto f(a). We say:
– Injective (one‐to‐one):
f(a)=f(a′)⟹a=a′f(a)=f(a')\implies a=a'.
– Surjective (onto):
∀b∈B.∃a.f(a)=b\forall b\in B.\;\exists a.\;f(a)=b.
– Bijective: both injective and surjective.
Composition of functions g∘f:A→Cg\circ f\colon A\to C is defined pointwise: (g∘f)(a)=g(f(a))(g\circ f)(a)=g(f(a)). The identity function on AA is 𝑖𝑑A(a)=a\mathit{id}_A(a)=a.
2 Algebraic Structures
2.1 Signatures and Universal Algebras
A signature Σ=(S,𝑎𝑟)\Sigma=(S,\mathit{ar}) consists of a set SS of operation symbols and an arity function 𝑎𝑟:S→ℕ\mathit{ar}:S\to\mathbb{N} assigning each symbol its number of arguments.
A
Σ\Sigma‐algebra
𝒜\mathcal A
comprises: • A carrier set
AA.
• For each
f∈Sf\in S
with
𝑎𝑟(f)=n\mathit{ar}(f)=n,
an operation
f𝒜:An→A.f^{\mathcal A}:A^n\to A.
A homomorphism h:𝒜→ℬh\colon \mathcal A\to\mathcal B between two Σ\Sigma‐algebras is a function h:A→Bh\colon A\to B preserving every operation: h(f𝒜(a1,…,an))=fℬ(h(a1),…,h(an)). h\bigl(f^{\mathcal A}(a_1,\dots,a_n)\bigr) \;=\; f^{\mathcal B}\bigl(h(a_1),\dots,h(a_n)\bigr). An initial algebra in the class of Σ\Sigma‐algebras is one from which there is a unique homomorphism into any other—this models inductive (free) data types.
- 2.2 Monoids
A monoid is a pair (M,*)(M,\ast) where MM is a set and *:M×M→M \ast\colon M\times M\to M is an associative binary operation with an identity element e∈Me\in M: ∀x,y,z∈M.(x*y)*z=x*(y*z),∀x.e*x=x=x*e. \forall x,y,z\in M.\;(x\ast y)\ast z = x\ast(y\ast z), \quad \forall x.\;e\ast x = x = x\ast e.
Examples:
–
(ℕ,+)(\mathbb{N},+)
with
00
as identity.
– Strings over an alphabet
Σ\Sigma:
(Σ*,𝑐𝑜𝑛𝑐𝑎𝑡,ε)(\Sigma^*,\mathit{concat},\varepsilon).
In Haskell one captures this as:
class Monoid m where
mempty :: m
mappend :: m -> m -> mappend
-- laws (not enforced by compiler):
-- mappend mempty x = x
-- mappend x mempty = x
-- mappend x (mappend y z) = mappend (mappend x y) z2.3 Lattices
A lattice is a set LL equipped with two binary operations, ∨,∧:L×L→L, \vee,\wedge \colon L\times L\to L, called join and meet, satisfying for all x,y,z∈Lx,y,z\in L:Commutativity: x∨y=y∨xx\vee y = y\vee x, x∧y=y∧xx\wedge y = y\wedge x.
Associativity: (x∨y)∨z=x∨(y∨z)(x\vee y)\vee z = x\vee(y\vee z), etc.
Absorption: x∨(x∧y)=xx\vee(x\wedge y)=x, x∧(x∨y)=xx\wedge(x\vee y)=x.
Equivalently, (L,≤)(L,\le) is a partial order in which every pair has a least upper bound (join) and greatest lower bound (meet). Example: (𝒫(A),⊆)(\mathcal P(A),\subseteq) with X∨Y=X∪Y,X∧Y=X∩Y. X\vee Y = X\cup Y, \quad X\wedge Y = X\cap Y.
3 Types as Sets and Algebraic Data Types
3.1 Types as Sets of Values
In a denotational semantics one assigns to each type τ\tau a set of values |τ||\tau|. The usual connectives correspond to set‐theoretic constructions:
• Product type:
|τ1×τ2|=|τ1|×|τ2|.|\tau_1\times\tau_2| \;=\; |\tau_1|\times|\tau_2|.
• Sum type (disjoint union):
|τ1+τ2|=|τ1|⊎|τ2|.|\tau_1+\tau_2| \;=\; |\tau_1|\;\uplus\;|\tau_2|.
• Function type:
|τ1→τ2|=|τ2||τ1|.|\tau_1\to\tau_2| \;=\; |\tau_2|^{\,|\tau_1|}.
Cardinalities satisfy |τ1×τ2|=|τ1|⋅|τ2|,|τ1+τ2|=|τ1|+|τ2|. |\tau_1\times\tau_2| = |\tau_1|\cdot|\tau_2|, \quad |\tau_1+\tau_2| = |\tau_1| + |\tau_2|.
- 3.2 Algebraic (Inductive) Data Types
An algebraic data type is given by constructors whose arities form a signature; the type is interpreted as the initial algebra of that signature. For example, in Haskell:
Signature: S={𝑁𝑜𝑡h𝑖𝑛𝑔,𝐽𝑢𝑠𝑡}S=\{\mathit{Nothing},\,\mathit{Just}\} with 𝑎𝑟(𝑁𝑜𝑡h𝑖𝑛𝑔)=0\mathit{ar}(\mathit{Nothing})=0, 𝑎𝑟(𝐽𝑢𝑠𝑡)=1\mathit{ar}(\mathit{Just})=1. Its carrier |𝑀𝑎𝑦𝑏𝑒A|={⊥}∪A|\mathit{Maybe}\,A|=\{\bot\}\cup A.
List example:
Signature
Σ𝐿𝑖𝑠𝑡\Sigma_{\mathit{List}}:
–
𝑁𝑖𝑙\mathit{Nil}
of arity
00.
–
𝐶𝑜𝑛𝑠\mathit{Cons}
of arity
22.
|𝐿𝑖𝑠𝑡A||\mathit{List}\,A| is the smallest set LL such that $$ \Nil\in L \quad\text{and}\quad (x\in A,\;xs\in L)\;\Rightarrow\;\Cons(x,xs)\in L. $$
- 3.3 Example: Binary Trees
In OCaml:
The signature has two constructors: –
𝐿𝑒𝑎𝑓:A→T\mathit{Leaf}\colon A\to T.
–
𝑁𝑜𝑑𝑒:T×T→T\mathit{Node}\colon T\times T\to T.
By universal‐algebra, TT is the initial Σ\Sigma‐algebra, so every other Σ\Sigma‐algebra receives a unique homomorphism from TT. This underpins fold‐like recursion schemes.
3.4 Cardinality and Infinity
If AA is infinite then so are many constructed types (e.g. AnA^n, A*A^*). Recursive types may denote least fixed points of functors F(X)=1+A×X, F(X) = 1 + A\times X, with solution X=μF≅⨄n≥0AnX = \mu F \cong \biguplus_{n\ge0} A^n (the set of finite lists).4 Chapter Summary
– We recalled set‐theoretic notation: unions, intersections, power
sets, relations and functions (injective/surjective/bijective).
– We introduced universal‐algebraic signatures,
Σ\Sigma‐algebras,
homomorphisms and initial algebras.
– We defined monoids and lattices, key structures in both mathematics
and program‐analysis (e.g. type lattices).
– We showed how programming‐language types correspond to set constructs
(products, sums, exponentials) and to initial algebras of signatures
(inductive types).
In Chapter 3 we will enrich this picture by showing how types and terms form categories, how simply typed λ\lambda‐calculus lives in a cartesian closed category, and how monads capture computational effects.
- –
In this chapter we introduce the basic notions of category theory—categories, functors and natural transformations—and show how they provide an elegant framework for understanding type theory. We then explain Cartesian closed categories (CCCs) and their exact correspondence with the simply‐typed λ‐calculus. Finally, we present monads (and comonads) as categorical abstractions of computational effects.
1 Categories, Functors and Natural Transformations
1.1 Definition of a Category
A category 𝒞\mathcal{C} consists of: • A class of objects Ob(𝒞)\mathrm{Ob}(\mathcal{C}).
• For each A,B∈Ob(𝒞)A,B\in \mathrm{Ob}(\mathcal{C}), a set of morphisms (or arrows)
𝒞(A,B)={f:A→B}.\mathcal{C}(A,B)\;=\;\{\,f\colon A\to B\,\}.
• For each A,B,CA,B,C, a composition operation
∘:𝒞(B,C)×𝒞(A,B)→𝒞(A,C),\circ\colon \mathcal{C}(B,C)\times\mathcal{C}(A,B)\;\to\;\mathcal{C}(A,C),
written (g,f)↦g∘f(g,f)\mapsto g\circ f.
• For each object AA, an identity morphism
idA:A→A.\mathrm{id}_A\colon A\to A.
These data satisfy the laws:
(Cat‐Assoc) (h∘g)∘f=h∘(g∘f)\quad (h\circ g)\circ f \;=\; h\circ (g\circ f)
(Cat‐Id) idB∘f=f=f∘idA\quad \mathrm{id}_B\circ f = f = f\circ \mathrm{id}_A
for all composable f,g,hf,g,h.
- 1.2 Examples of Categories
– Set: objects are all sets; morphisms are total
functions.
– Hask: in Haskell, types as objects, total (pure)
Haskell functions as morphisms (ignoring bottoms).
– Rel: objects are sets; morphisms
R:A→BR\colon A\to B
are binary relations
R⊆A×BR\subseteq A\times B,
composed by relational composition.
- 1.3 Functors
A functor F:𝒞→𝒟F\colon \mathcal{C}\to\mathcal{D} between categories assigns:
• To each object
A∈Ob(𝒞)A\in\mathrm{Ob}(\mathcal{C}),
an object
F(A)∈Ob(𝒟)F(A)\in\mathrm{Ob}(\mathcal{D}).
• To each morphism
f:A→Bf\colon A\to B,
a morphism
F(f):F(A)→F(B)F(f)\colon F(A)\to F(B)
preserving identities and composition:
F(idA)=idF(A),F(g∘f)=F(g)∘F(f). F(\mathrm{id}_A) = \mathrm{id}_{F(A)}, \quad F(g\circ f) = F(g)\circ F(f).
Example. The power‐set functor 𝒫:𝐒𝐞𝐭→𝐒𝐞𝐭\mathcal P\colon \mathbf{Set}\to\mathbf{Set} sends A↦𝒫(A),f:A→B↦𝒫(f):𝒫(A)→𝒫(B),𝒫(f)(X)={f(x)∣x∈X}. A \;\mapsto\; \mathcal P(A), \quad f\colon A\to B \;\mapsto\; \mathcal P(f)\colon \mathcal P(A)\to\mathcal P(B), \quad \mathcal P(f)(X)=\{\,f(x)\mid x\in X\}.
- 1.4 Natural Transformations
Given parallel functors F,G:𝒞→𝒟F,G\colon \mathcal{C}\to\mathcal{D}, a natural transformation
η:F⇒G\eta\colon F\Rightarrow G
assigns to each A∈Ob(𝒞)A\in\mathrm{Ob}(\mathcal{C}) a morphism
ηA:F(A)→G(A)\eta_A\colon F(A)\to G(A)
such that for every f:A→Bf\colon A\to B in 𝒞\mathcal{C} the following naturality square commutes: $$ \begin{CD} F(A) @>F(f)>> F(B) \\ @V\eta_AVV @VV\eta_B V \\ G(A) @>G(f)>> G(B) \end{CD} $$
Example. In Set, the inclusion ι:X↪𝒫(X)\iota\colon X\hookrightarrow \mathcal P(X) (sending x↦{x}x\mapsto\{x\}) is a natural transformation Id⇒𝒫\mathrm{Id}\Rightarrow\mathcal P.
2 Cartesian Closed Categories ↔\longleftrightarrow Simply‐Typed λ‐Calculus
2.1 Products and Terminal Object
A category 𝒞\mathcal{C} has a terminal object 11 if for every AA there is a unique morphism
!A:A→1.!_A\colon A\to 1. A product of A,BA,B is an object A×BA\times B equipped with projections
π1:A×B→A,π2:A×B→B\pi_1\colon A\times B\to A,\quad \pi_2\colon A\times B\to B
universal in the sense that for any CC and f:C→Af\colon C\to A, g:C→Bg\colon C\to B, there is a unique
⟨f,g⟩:C→A×B\langle f,g\rangle\colon C\to A\times B
making π1∘⟨f,g⟩=f\pi_1\circ\langle f,g\rangle = f and π2∘⟨f,g⟩=g\pi_2\circ\langle f,g\rangle = g.2.2 Exponentials
Given objects A,BA,B, an exponential BAB^A (if it exists) is equipped with an evaluation morphism
ev:BA×A→B\mathrm{ev}\colon B^A\times A \;\to\; B
such that for every f:C×A→Bf\colon C\times A\to B there is a unique
Λ(f):C→BA\Lambda(f)\colon C\;\to\; B^A
making the diagram commute: $$ \begin{CD} C\times A @>f>> B \\ @V\Lambda(f)\times \mathrm{id}_A VV @| \\ B^A\times A @>\mathrm{ev}>> B \end{CD} $$2.3 Definition of a Cartesian Closed Category (CCC)
A category is cartesian closed if it has:A terminal object 11.
Binary products A×BA\times B for all A,BA,B.
Exponentials BAB^A for all A,BA,B.
2.4 CCC ↔︎ Simply‐Typed λ‐Calculus
There is an equivalence:
• In the simply‐typed λ‐calculus (STLC), types
τ\tau
are objects, contexts
Γ\Gamma
give products, and terms
M:Γ⊢τM\colon \Gamma\vdash\tau
correspond to morphisms
M:|Γ|=∏x:σ∈Γσ→τ.M\colon |\Gamma|\;=\;\prod_{x:\sigma\in\Gamma}\sigma\;\longrightarrow\;\tau.
• Composition of morphisms models term substitution; identity morphisms
are variables.
•
λ\lambda‐abstraction
corresponds to
Λ\Lambda
(currying), application to
ev\mathrm{ev}
(evaluation).
Thus the category 𝐒𝐓𝐋𝐂\mathbf{STLC} of types-and-terms is a CCC. Conversely, every CCC gives rise to a typed λ‐calculus.
- 2.5 Curry–Howard–Lambek Correspondence
The classic trinity:
• Propositional logic with
×,→\times,\to.
• Simply‐typed λ‐calculus with product types and function types.
• Cartesian closed categories.
Under this, proof‐derivation = λ‐term = morphism.
3 Monads, Comonads and Computational Effects
3.1 Definition of a Monad
A monad on a category 𝒞\mathcal{C} is a triple (T,η,μ)(T,\eta,\mu) where
• T:𝒞→𝒞T\colon \mathcal{C}\to\mathcal{C} is an endofunctor.
• η:Id⇒T\eta\colon \mathrm{Id}\Rightarrow T (unit) and μ:T2⇒T\mu\colon T^2\Rightarrow T (multiplication) are natural transformations satisfying:Associativity:
μA∘T(μA)=μA∘μT(A). \mu_A\circ T(\mu_A) = \mu_A\circ \mu_{T(A)}.Unit laws:
μA∘T(ηA)=idT(A),μA∘ηT(A)=idT(A). \mu_A\circ T(\eta_A) = \mathrm{id}_{T(A)} \;,\quad \mu_A\circ \eta_{T(A)} = \mathrm{id}_{T(A)}.3.2 Kleisli and Eilenberg–Moore
– The Kleisli category 𝒞T\mathcal{C}_T: same objects as 𝒞\mathcal{C}, morphisms A→BA\to B are A→T(B)A\to T(B) in 𝒞\mathcal{C}.
– Kleisli extension (−)*(-)^\ast: for f:A→T(B)f\colon A\to T(B), obtain f*:T(A)→T(B)f^\ast\colon T(A)\to T(B).3.3 Examples of Monads
– Maybe monad in Hask:
T(A)=A+1,η(a)=𝖩𝗎𝗌𝗍a,μ(𝖩𝗎𝗌𝗍x)=x,μ(𝖭𝗈𝗍𝗁𝗂𝗇𝗀)=𝖭𝗈𝗍𝗁𝗂𝗇𝗀.T(A)=A+1,\quad \eta(a)=\mathsf{Just}\;a,\quad \mu(\mathsf{Just}\,x)=x,\;\mu(\mathsf{Nothing})=\mathsf{Nothing}.
– List monad:
T(A)=A*T(A)=A^*,
η(a)=[a]\eta(a)=[a],
μ=𝖼𝗈𝗇𝖼𝖺𝗍\mu=\mathsf{concat}.
– State monad:
T(A)=S→(A×S)T(A)=S\to (A\times S).
- 3.4 Haskell Example
+ - Maybe monad
instance Monad Maybe where
return x = Just x
Nothing >>= _ = Nothing
(Just x) >>= k = k x
+ - List monad
instance Monad [] where
return x = [x]
xs >>= k = concat (map k xs)3.5 Monads in Semantics of Computation
Moggi’s insight: monads encapsulate computational effects—state, exceptions, nondeterminism, I/O—while preserving a pure core. One endows a “computational λ‐calculus” with type constructor T(τ)T(\tau) for effectful computations.3.6 Comonads
Dually, a comonad is (W,ε,δ)(W,\varepsilon,\delta) with W:𝒞→𝒞W\colon\mathcal{C}\to\mathcal{C}, counit ε:W⇒Id\varepsilon\colon W\Rightarrow\mathrm{Id}, comultiplication δ:W⇒W2\delta\colon W\Rightarrow W^2 satisfying dual laws. The coKleisli category models context‐dependent computations.3.7 Example: Reader Comonad
In a language with a fixed environment EE, define
W(A)=E→A,ε(f)=f(e0),δ(f)(e)=λe′.f(e′).W(A)=E\to A,\quad \varepsilon(f)=f(e_0),\quad \delta(f)(e)=\lambda e'.\,f(e').
This comonad represents read‐only context passing.4 Chapter Summary
– We defined categories, functors and natural transformations.
– We showed that Cartesian closed categories precisely model the
simply‐typed λ‐calculus.
– We introduced monads as categorical abstractions of computational
effects and sketched Kleisli semantics.
– We briefly sketched comonads for context‐sensitive computations.
In Chapter 4 we turn to combinatory logic—an alternative variable‐free foundation of computation—and relate its typed variants back to the λ‐calculus and categorical models.
- –
In this chapter we present Combinatory Logic (CL), a variable‐free formulation of computation invented by Schönfinkel and Curry. We introduce the basic SKI system, develop its simply‐typed variant, and prove its equivalence with the simply‐typed λ‐calculus. Along the way we show how combinatory reduction can be implemented in practice and how combinatory algebras arise as categorical models.
1 The Untyped SKI Combinators
1.1 Syntax and Reduction Rules
Terms of the SKI‐calculus are built from three primitive combinators 𝐒,𝐊,𝐈\mathbf{S},\mathbf{K},\mathbf{I} and application: M,N::=𝐒∣𝐊∣𝐈∣MN M,N ::= \mathbf{S}\mid \mathbf{K}\mid \mathbf{I} \mid M\;N Reduction is effected by the rules: 𝐊MN→M,𝐒MNP→MP(NP),𝐈M→M. \begin{aligned} \mathbf{K}\;M\;N &\;\to\; M,\\ \mathbf{S}\;M\;N\;P &\;\to\; M\;P\;(N\;P),\\ \mathbf{I}\;M &\;\to\; M. \end{aligned} Here application associates to the left: MNPQ≡(((MN)P)Q)MNPQ\equiv(((M\,N)\,P)\,Q).1.2 Expressiveness: Eliminating Variables
Every λ‐term tt can be translated into an equivalent SKI‐term [t][t] satisfying [λx.t]N→*t[N/x]. [\lambda x.\,t]\;N \;\to^*\; t[N/x]. The usual translation [[⋅]][\![\,\cdot\,]\!] is defined by:[[x]]=x[\![x]\!] = x (treated as a nullary combinator or variable).
[[MN]]=[[M]][[N]][\![M\,N]\!] = [\![M]\!]\;[\![N]\!].
[[λx.M]]=𝐊[[M]][\![\lambda x.\,M]\!] = \mathbf{K}\,[\![M]\!] if x∉𝐹𝑉(M)x\notin\mathit{FV}(M);
[[λx.x]]=𝐈[\![\lambda x.\,x]\!] = \mathbf{I};
[[λx.MN]]=𝐒[[λx.M]][[λx.N]][\![\lambda x.\,M\,N]\!] = \mathbf{S}\,[\![\lambda x.\,M]\!]\,[\![\lambda x.\,N]\!].
1.3 Implementation: A Simple C Reducer
Below is a sketch of a C program that represents combinators and performs head‐reduction.
// skicomb.c
#include <stdio.h>
#include <stdlib.h>
typedef enum { S_COMB, K_COMB, I_COMB, APP } Tag;
typedef struct Term Term;
struct Term {
Tag tag;
Term *left, *right;
};
Term* make(Tag t, Term* l, Term* r) {
Term* p = malloc(sizeof *p);
p->tag = t; p->left = l; p->right = r;
return p;
}
Term* reduce(Term* t) {
if (t->tag==APP && t->left->tag==K_COMB) {
// K M N → M
return t->left->right;
}
if (t->tag==APP && t->left->tag==APP &&
t->left->left->tag==S_COMB) {
// S M N P → M P (N P)
Term *M = t->left->right;
Term *N = t->right;
Term *P = t->right; // careful: P = t->right
Term *NP = make(APP,N,P);
return make(APP, make(APP,M,P), NP);
}
if (t->tag==APP && t->left->tag==I_COMB) {
// I M → M
return t->right;
}
// no rule applies
return t;
}
int main(){
// Example: ((S K) K) x reduces to x
Term *x = make(APP, make(K_COMB,0,0), make(K_COMB,0,0));
// omitted full build / loop
}2 Simply‐Typed Combinatory Calculus
2.1 Types and Typing Rules
We decorate SKI with simple types τ\tau generated by τ::=α∣τ1→τ2, \tau ::= \alpha\mid \tau_1\to\tau_2, where α\alpha ranges over base‐type atoms. Typing judgments have the form ⊢M:τ. \vdash M:\tau. We impose the following rules:
(Var)
$$
\infer{\vdash x:\tau}{x:\tau\in\Gamma}
$$
$$ \infer{\vdash \mathbf{K}:\tau_1\to\tau_2\to\tau_1}{} $$ $$ \infer{\vdash \mathbf{S}:(\tau_1\to\tau_2\to\tau_3)\to(\tau_1\to\tau_2)\to \tau_1\to\tau_3}{} $$
$$ \infer{\vdash \mathbf{I}:\tau\to\tau}{} $$
(App)
$$
\infer{\vdash M\;N:\tau_2}
{\vdash M:\tau_1\to\tau_2
\quad
\vdash N:\tau_1}
$$
2.2 Example Derivation
Prove ⊢𝐒𝐊𝐊:α→α\vdash \mathbf{S}\,\mathbf{K}\,\mathbf{K}:\alpha\to\alpha.By (K), ⊢𝐊:α→β→α\vdash \mathbf{K}:\alpha\to\beta\to\alpha.
By (K) (instantiating β=α\beta=\alpha), ⊢𝐊:α→α→α\vdash \mathbf{K}:\alpha\to\alpha\to\alpha.
By (S),
⊢𝐒:(α→α→α)→(α→α)→α→α\vdash \mathbf{S}:(\alpha\to\alpha\to\alpha)\to(\alpha\to\alpha)\to\alpha\to\alpha.Apply (App) twice to obtain
⊢𝐒𝐊𝐊:α→α\vdash \mathbf{S}\,\mathbf{K}\,\mathbf{K}:\alpha\to\alpha.3 Equivalence with Simply‐Typed λ‐Calculus
3.1 Translation from CL to λ‐Calculus
Define Φ(M)\Phi(M) as the λ‐term corresponding to CL‐term MM by mapping Φ(𝐒)=λxyz.xz(yz),Φ(𝐊)=λxy.x,Φ(𝐈)=λx.x, \Phi(\mathbf{S}) = \lambda x y z.\;x\,z\,(y\,z), \quad \Phi(\mathbf{K}) = \lambda x y.\;x, \quad \Phi(\mathbf{I}) = \lambda x.\;x, and Φ(MN)=Φ(M)Φ(N)\Phi(M\,N)=\Phi(M)\,\Phi(N). One shows:
Theorem (Soundness)
If
⊢CLM:τ\vdash_{\mathrm{CL}} M:\tau
then
⊢λΦ(M):τ\vdash_{\lambda} \Phi(M):\tau.
- 3.2 Translation from λ‐Calculus to CL
Conversely, map each λ‐abstraction to SKI via the translation of §4.1.2. Then:
Theorem (Completeness)
If
Γ⊢λt:τ\Gamma\vdash_{\lambda} t:\tau
then
⊢CL[[t]]:τ\vdash_{\mathrm{CL}} [\![t]\!]:\tau.
3.3 Adequacy of Translations
Combining soundness and completeness yields an isomorphism of derivability and preserved reduction: [[Φ(M)]]→CL*M,Φ([[t]])→λ*t. [\![\Phi(M)]\!] \;\to^*_{\mathrm{CL}}\; M, \quad \Phi([\![t]\!]) \;\to^*_{\lambda}\; t.4 Combinatory Algebras and Categorical Models
4.1 Combinatory Algebra
A combinatory algebra is a set AA with a binary application operation ⋅\cdot and distinguished elements s,k∈As,k\in A satisfying:s⋅x⋅y⋅z=x⋅z⋅(y⋅z)s\cdot x\cdot y\cdot z = x\cdot z\cdot (y\cdot z)
k⋅x⋅y=xk\cdot x\cdot y = x
Such an algebra models CL and yields a categorical model by taking objects as types and morphisms A→BA\to B as the set {f∈A∣∀x∈A,f⋅x∈B}. \{\,f\in A \mid \forall x\in A,\;f\cdot x\in B\}.
4.2 Categorical Perspective
Every CCC yields a combinatory algebra by collapsing the CCC’s morphisms into an applicative structure. Conversely, from a combinatory algebra with enough “abstract” points one constructs a CCC of partial equivalence relations.5 Programming with Combinators
5.1 Scheme Example: Combinator Interpreter
(define (I x) x)
(define (K x) (lambda (y) x))
(define (S x) (lambda (y) (lambda (z)
((x z) ((y z))))))
(define (eval-sk m)
(cond ((procedure? m) m)
((pair? m) ; application
(let ((f (eval-sk (car m)))
(a (eval-sk (cadr m))))
(f a)))
(else (error "Unknown term" m))))- 5.2 Haskell Example: SKI as Data Type
data SKI = S | K | I | App SKI SKI
reduce :: SKI -> SKI
reduce (App (App (App S m) n) p) = App (App m p) (App n p)
reduce (App (App K m) _) = m
reduce (App I m) = m
reduce t = t- 6 Chapter Summary
– We introduced the untyped SKI combinators and showed how they
eliminate variables.
– We equipped SKI with simple types and gave typing rules for
𝐒,𝐊,𝐈\mathbf{S},\mathbf{K},\mathbf{I}.
– We proved equivalence with the simply‐typed λ‐calculus via
bidirectional translations.
– We outlined the notion of a combinatory algebra and its connection to
categorical models.
– We provided concrete implementations in C, Scheme and Haskell.
In Chapter 5 we return to the λ‐calculus itself, formalize its operational semantics and develop richer type systems including products, sums and recursive types.
- –
In this chapter we develop the untyped λ‐calculus—the foundational model of computation—and then introduce its typed variants. We cover syntax, α/β/η‐conversion, operational semantics, Church encodings of data, the simply‐typed λ‐calculus (STLC), principal‐type inference (Hindley–Milner / Algorithm W), and an introduction to second‐order polymorphism (System F).
1 The Untyped λ‐Calculus
1.1 Syntax
Terms M,NM,N are given by the grammar M,N::=x∣λx.M∣MN M,N ::= x \mid \lambda x.\,M \mid M\,N where xx ranges over a countable set of variables.1.2 α‐Conversion and Capture‐Avoiding Substitution
– α‐equivalence (M≡αNM\equiv_\alpha N) identifies renamings of bound variables.
– Capture‐avoiding substitution M[N/x]M[N/x] replaces free occurrences of xx in MM by NN, renaming bound variables in MM as needed to avoid capture.1.3 β‐Reduction and η‐Reduction
– β‐reduction: (λx.M)N→βM[N/x](\lambda x.\,M)\,N \;\to_\beta\; M[N/x].
– η‐reduction: λx.Mx→ηM\lambda x.\,M\,x \;\to_\eta\; M when x∉𝐹𝑉(M)x\notin\mathit{FV}(M).
We write →*\to^* for the reflexive‐transitive closure of →β∪→η\to_\beta\cup\to_\eta.1.4 Operational Semantics and Strategies
– Normal‐order (leftmost‐outermost) vs applicative‐order (leftmost‐innermost).
– Head‐reduction computes head‐normal form if it exists.1.5 Church Encodings of Data
1.5.1 Booleans
𝗍𝗋𝗎𝖾=λtf.t,𝖿𝖺𝗅𝗌𝖾=λtf.f. \mathsf{true} = \lambda t f.\,t,\quad \mathsf{false} = \lambda t f.\,f. Define 𝗂𝖿M𝗍𝗁𝖾𝗇N𝖾𝗅𝗌𝖾P=MNP\mathsf{if}\;M\;\mathsf{then}\;N\;\mathsf{else}\;P = M\,N\,P.1.5.2 Church Numerals
n¯=λsz.snz, \overline{n} = \lambda s z.\;s^n\,z, with successor and addition: 𝗌𝗎𝖼𝖼=λnsz.s(nsz),𝗉𝗅𝗎𝗌=λmnsz.ms(nsz). \mathsf{succ} = \lambda n s z.\,s\,(n\,s\,z),\quad \mathsf{plus} = \lambda m n s z.\,m\,s\,(n\,s\,z).1.5.3 Pairs
⟨M,N⟩=λp.pMN,𝖿𝗌𝗍=λp.p(λxy.x),𝗌𝗇𝖽=λp.p(λxy.y). \langle M,N\rangle = \lambda p.\,p\,M\,N,\quad \mathsf{fst} = \lambda p.\,p\,(\lambda x y.\,x),\quad \mathsf{snd} = \lambda p.\,p\,(\lambda x y.\,y).1.6 Example: A Small Evaluator in Scheme
;; untyped λ‐calculus evaluator (very naive)
(define (subst body x val)
(match body
[(var y) (if (eq? y x) val body)]
[(lam y m) (if (eq? y x) body
(lam y (subst m x val)))]
[(app m n) (app (subst m x val) (subst n x val))]))
(define (step term)
(match term
[(app (lam x m) n) (subst m x n)] ; β‐reduction
[(app m n) (app (step m) n)]
[else term]))
(define (eval term)
(let loop ([t term])
(let ([t' (step t)])
(if (eqv? t t') t (loop t')))))2 Simply‐Typed λ‐Calculus (STLC)
2.1 Types and Terms
Types τ\tau and terms MM are given by τ::=α∣τ1→τ2,M::=x∣λx:τ.M∣MN. \tau ::= \alpha \mid \tau_1\to\tau_2, \qquad M ::= x \mid \lambda x\!:\!\tau.\,M \mid M\,N.2.2 Typing Contexts and Judgments
A context Γ\Gamma is a finite map from variables to types. Typing judgment: Γ⊢M:τ. \Gamma\vdash M:\tau.2.3 Inference Rules
[ {x!:!} {,x!:!_1;;M:_2} ] [ {M:_1_2 N:_1} ]2.4 Type Safety
The key metatheoretic properties are:
(Progress) If ⌀⊢M:τ\varnothing\vdash M:\tau then either MM is a value (λ\lambda‐abstraction) or M→M′M\to M'.
(Preservation) If Γ⊢M:τ\Gamma\vdash M:\tau and M→M′M\to M' then Γ⊢M′:τ\Gamma\vdash M':\tau.
Together they imply type safety (no stuck well‐typed terms).
- 2.5 Example Typing in OCaml
(* identity *)
let id (x : 'a) : 'a = x
(* composition *)
let compose (f : 'b -> 'c) (g : 'a -> 'b) (x : 'a) : 'c =
f (g x)3 Principal‐Type Inference: Hindley–Milner and Algorithm W
3.1 Type Schemes and Generalization
– A type scheme is ∀α1…αn.τ\forall\alpha_1\dots\alpha_n.\,\tau.
– Generalization 𝗀𝖾𝗇(Γ,τ)\mathsf{gen}(\Gamma,\tau) quantifies over type variables in τ\tau not free in Γ\Gamma.3.2 Algorithm W Outline
Given Γ\Gamma and term MM, computes (S,τ)(S,\tau) where SS is a substitution and τ\tau a type such that SΓ⊢M:τS\Gamma\vdash M:\tau, and τ\tau is principal.3.3 Example in Standard ML
4 Polymorphic λ‐Calculus (System F)
4.1 Syntax and Types
Types and terms: τ::=α∣τ1→τ2∣∀α.τ,M::=x∣λx:τ.M∣MN∣Λα.M∣M[τ]. \tau ::= \alpha \mid \tau_1\to\tau_2 \mid \forall\alpha.\,\tau, \quad M ::= x \mid \lambda x\!:\!\tau.\,M \mid M\,N \mid \Lambda\alpha.\,M \mid M\,[\tau].4.2 Typing Rules
[ {M: ()} {M : .,} ]4.3 Encodings and Expressiveness
System F can type‐safe encode Church numerals, booleans, pairs, lists, etc., without ad hoc combinators.5 Chapter Summary
– We defined the untyped λ‐calculus: syntax, α/β/η‐conversion,
evaluation strategies, Church encodings.
– We introduced the simply‐typed λ‐calculus (STLC), its typing rules,
and proved type safety (progress & preservation).
– We sketched Hindley–Milner principal‐type inference (Algorithm W) and
gave ML/OCaml examples.
– We presented the polymorphic λ‐calculus (System F) with universal
quantification.
In Chapter 6 we extend these calculi with inductive and coinductive types, explore pattern matching, and develop their categorical and semantic underpinnings.
- –
In this chapter we extend the simply‐typed λ‐calculus with record types and introduce a subtyping relation to allow safe reuse of records with more fields or more specific field types. We cover
• Syntax and typing of record expressions
• The subtyping relation
<:<:\,:
reflexivity, transitivity, top type, arrow subtyping, and three forms of
record subtyping (width, depth, permutation)
• Typing rules with subsumption
• Examples in OCaml and TypeScript
• Preservation and progress in the presence of subtyping
1 Motivation for Subtyping
Many programming‐language features benefit from being able to treat a value of one type as a value of a “bigger” or “more general” type. In particular:
– A record with extra fields can safely be used when only a subset of fields is needed (width subtyping).
– A record whose field types are more specific can be used where a more general field type is expected (depth subtyping).
– Fields may be listed in any order (permutation subtyping).2 Syntax and Static Semantics
2.1 Types
Extend types τ\tau by record types: τ::=α∣τ1→τ2∣{li:τi}i=1n∣⊤ \tau ::= \alpha \mid \tau_1\to\tau_2 \mid \{\;l_i:\tau_i\}_{i=1}^n \mid \top Here {li:τi}\{l_i:\tau_i\} is a record type with labels l1,…,lnl_1,\dots,l_n, and ⊤\top is the “top” type, supertype of all types.2.2 Terms
Extend terms MM by record formation and projection: M::=x∣λx:τ.M∣MN∣{li=Mi}i=1n∣M.l M ::= x \mid \lambda x\!:\!\tau.\,M \mid M\;N \mid \{\,l_i=M_i\}_{i=1}^n \mid M.l2.3 Values
Values vv are: v::=λx:τ.M∣{li=vi}i=1n. v ::= \lambda x\!:\!\tau.\,M \mid \{\,l_i=v_i\}_{i=1}^n.3 The Subtyping Relation
We write S<:TS<:T when SS is a subtype of TT. The rules are:
(T‐Refl)
$$
\infer
{T<:T}
{}
$$
(T‐Trans)
$$
\infer
{S<:U}
{S<:T \quad T<:U}
$$
(T‐Top)
$$
\infer
{S<:\top}
{}
$$
(T‐Arrow)
$$
\infer
{S_1\to S_2<:T_1\to T_2}
{T_1<:S_1 \quad S_2<:T_2}
$$ Note: function types are contravariant in the domain and
covariant in the codomain.
(T‐RcdWidth)
If
{li:Si}i=1n\{\,l_i:S_i\}_{i=1}^n
has at least the labels
l1,…,lkl_1,\dots,l_k
then $$
\infer
{\{\,l_i:S_i\}_{i=1}^n \;<:\;\{\,l_i:S_i\}_{i=1}^k}
{}
$$
(T‐RcdDepth)
$$
\infer
{\{\,l_i:S_i\}_{i=1}^n \;<:\;\{\,l_i:T_i\}_{i=1}^n}
{ \forall i.\;S_i<:T_i }
$$
(T‐RcdPerm)
If
(j1,…,jn)(j_1,\dots,j_n)
is a permutation of
(1,…,n)(1,\dots,n)
then $$
\infer
{\{\,l_{j_i}:S_{j_i}\}_{i=1}^n \;<:\;\{\,l_i:S_i\}_{i=1}^n}
{}
$$
Together, these let us drop fields (width), replace each field by a supertype (depth), and ignore ordering (permutation).
- 4 Typing Rules with Subsumption
Extend the standard STLC rules with record formation and projection, plus subsumption:
(Var)
$$
\infer
{\Gamma\vdash x:\tau}
{x:\tau\in\Gamma}
$$
(Abs)
$$
\infer
{\Gamma\vdash \lambda x:\!S.\,M : S\to T}
{\Gamma,x:S\vdash M:T}
$$
(App)
$$
\infer
{\Gamma\vdash M\,N : T}
{\Gamma\vdash M : S\to T
\quad
\Gamma\vdash N : S}
$$
(Rcd)
$$
\infer
{\Gamma\vdash \{\,l_i=M_i\}_{i=1}^n : \{\,l_i:\tau_i\}_{i=1}^n}
{\forall i.\;\Gamma\vdash M_i:\tau_i}
$$
(Proj)
$$
\infer
{\Gamma\vdash M.l_j : \tau_j}
{\Gamma\vdash M:\{\,l_i:\tau_i\}_{i=1}^n \quad j\le n}
$$
(Subsumption)
$$
\infer
{\Gamma\vdash M:S}
{\Gamma\vdash M:T
\quad
T<:S}
$$
5 Examples
5.1 OCaml Records and Width Subtyping (by Hand)
(* OCaml does not support structural subtyping directly, but we illustrate the idea *)
type person = { name : string; age : int }
type employee = { name : string; age : int; id : int }
let greet (p : person) =
"Hello, " ^ p.name ^ " age " ^ string_of_int p.age
let e = { name="Alice"; age=30; id=123 }
let s = greet e (* OK by width subtyping: employee <: person *)- 5.2 TypeScript Structural Subtyping
interface Person { name: string; age: number }
interface Employee { name: string; age: number; id: number }
function greet(p: Person): string {
return `Hello, ${p.name}, age ${p.age}`;
}
const e: Employee = { name: "Bob", age: 40, id: 999 };
const msg = greet(e); // OK: Employee <: Person by width subtyping- 5.3 Depth Subtyping Example
interface A { x: number }
interface B { x: 42 } // literal type 42 <: number
let b: B = { x: 42 };
let a: A = b; // OK: B <: A by depth subtyping- 6 Operational Semantics
Extend evaluation with record and projection:
(E‐Rcd)
{li=vi}i=1nis a value
\{\,l_i=v_i\}_{i=1}^n\; \text{is a value}
(E‐Proj)
$$
\infer
{ \{\,l_i=v_i\}_{i=1}^n . l_j \;\to\; v_j }
{}
$$
Plus congruence rules to evaluate subterms.
- 7 Type Safety with Subtyping
We state the usual theorems adapted to subsumption:
Theorem (Progress)
If
⌀⊢M:T\varnothing\vdash M:T
then either
MM
is a value or there is
M′M'
with
M→M′M\to M'.
Theorem (Preservation)
If
Γ⊢M:T\Gamma\vdash M:T
and
M→M′M\to M'
then
Γ⊢M′:T\Gamma\vdash M':T.
The proofs proceed by induction on the typing derivation. The only non‐standard case is subsumption, which uses transitivity of <:<:.
- 8 Extensions and Remarks
– Bounded quantification (System
F<:_{<:})
combines polymorphism with subtyping.
– Object types in OO languages generalize record subtyping with
methods.
– Row‐polymorphism gives more flexible ways to talk about records with
unknown extra fields.
- 9 Chapter Summary
– We added record types
{li:τi}\{l_i:\tau_i\}
and projection to the λ‐calculus.
– We defined a structural subtyping relation
<:<:\,
with reflexivity, transitivity, top, arrow subtyping, and three forms of
record subtyping: width, depth, and permutation.
– We extended the typing rules with a subsumption rule to allow
T<:ST<:S.
– We illustrated ideas in OCaml (by analogy) and TypeScript (structural
subtyping).
– We showed that progress and preservation still hold.
In Chapter 7 we will introduce sum types, variant types, and pattern matching, further enriching our typed λ‐calculi.
- –
In this chapter we explore parametric polymorphism, beginning with the second-order λ-calculus (System F), its syntax, typing and reduction rules, and demonstrating how it subsumes many ad hoc encodings of data. We then examine the theory of parametricity (Reynolds’s abstraction theorem and free theorems) and outline extensions such as existential types for data abstraction, bounded quantification (F<:), type operators (System Fω), and practical let-polymorphism as in ML and Haskell.
1 Overview of Polymorphism
• Monomorphic vs. preorder polymorphism vs. parametric polymorphism
• Importance: code reuse, data abstraction, generic libraries
• Two main styles
– Implicit “let-polymorphism” (Hindley–Milner)
– Explicit second-order polymorphism (System F)2 System F: Syntax and Operational Semantics
2.1 Types and Terms
Types and terms of System F extend STLC with universal quantification: τ::=α∣τ1→τ2∣∀α.τ \tau ::= \alpha \mid \tau_1 \to \tau_2 \mid \forall\alpha.\,\tau M::=x∣λx:τ.M∣MN∣Λα.M∣M[τ] M ::= x \mid \lambda x\!:\!\tau.\,M \mid M\,N \mid \Lambda\alpha.\,M \mid M\,[\tau]2.2 Reduction Rules
• β-reduction (term‐level):
(λx:τ.M)N→βM[N/x].(\lambda x\!:\!\tau.\,M)\,N \;\to_\beta\; M[N/x].
• β₂-reduction (type‐level):
(Λα.M)[τ]→β2M[τ/α].(\Lambda\alpha.\,M)\,[\tau] \;\to_{\beta2}\; M[\tau/\alpha].
• Congruence rules to reduce inside applications and type-applications.
We write →*\to^* for the reflexive–transitive closure of →β∪→β2\to_\beta\cup\to_{\beta2}.3 Typing System F
3.1 Contexts and Judgments
A typing context Γ\Gamma maps term variables to types and contains type-variable declarations. We write Γ⊢M:τ \Gamma \vdash M:\tau meaning under type‐variables in Γ\Gamma and term‐bindings in Γ\Gamma, term MM has type τ\tau.3.2 Inference Rules
(Var)
$$
\infer{\Gamma,x:\tau\vdash x:\tau}{}
$$
(Abs)
$$
\infer{\Gamma\vdash \lambda x\!:\!\tau_1.\,M : \tau_1\to\tau_2}
{\Gamma,x:\tau_1\vdash M:\tau_2}
$$
(App)
$$
\infer{\Gamma\vdash M\,N:\tau_2}
{\Gamma\vdash M:\tau_1\to\tau_2
\quad
\Gamma\vdash N:\tau_1}
$$
(Gen)
$$
\infer{\Gamma\vdash \Lambda\alpha.\,M : \forall\alpha.\,\tau}
{\Gamma,\alpha\text{ type}\vdash M:\tau}
$$
(Inst)
$$
\infer{\Gamma\vdash M\,[\sigma] : \tau[\sigma/\alpha]}
{\Gamma\vdash M : \forall\alpha.\,\tau}
$$
3.3 Examples of System F Terms
• Polymorphic identity:
𝗂𝖽=Λα.λx:α.x\mathsf{id} = \Lambda\alpha.\,\lambda x\!:\!\alpha.\,x
Has type ∀α.α→α\forall\alpha.\,\alpha\to\alpha.
• Polymorphic composition:
𝖼𝗈𝗆𝗉𝗈𝗌𝖾=Λα.Λβ.Λγ.λf:(β→γ).λg:(α→β).λx:α.f(gx)\mathsf{compose} = \Lambda\alpha.\Lambda\beta.\Lambda\gamma.\, \lambda f:(\beta\to\gamma).\, \lambda g:(\alpha\to\beta).\, \lambda x:\alpha.\,f\,(g\,x)
Has type ∀αβγ.(β→γ)→(α→β)→(α→γ)\forall\alpha\beta\gamma.\,(\beta\to\gamma)\to(\alpha\to\beta)\to(\alpha\to\gamma).4 Encoding Data in System F
4.1 Church Booleans and Conditionals
𝖡𝗈𝗈𝗅=∀α.α→α→α \mathsf{Bool} = \forall\alpha.\,\alpha\to\alpha\to\alpha 𝗍𝗋𝗎𝖾=Λα.λt:α.λf:α.t \mathsf{true} = \Lambda\alpha.\,\lambda t:\alpha.\,\lambda f:\alpha.\,t 𝖿𝖺𝗅𝗌𝖾=Λα.λt:α.λf:α.f \mathsf{false} = \Lambda\alpha.\,\lambda t:\alpha.\,\lambda f:\alpha.\,f4.2 Church Numerals
𝖭𝖺𝗍=∀α.(α→α)→α→α \mathsf{Nat} = \forall\alpha.\,(\alpha\to\alpha)\to\alpha\to\alpha n¯=Λα.λs:(α→α).λz:α.snz \overline{n} = \Lambda\alpha.\,\lambda s:(\alpha\to\alpha).\, \lambda z:\alpha.\,s^n\,z4.3 Pairs, Sums, Lists
Defined similarly via universal types: • 𝖯𝖺𝗂𝗋AB=∀α.(A→B→α)→α\mathsf{Pair}\,A\,B = \forall\alpha.\,(A\to B\to\alpha)\to\alpha.
• 𝖤𝗂𝗍𝗁𝖾𝗋AB=∀α.(A→α)→(B→α)→α\mathsf{Either}\,A\,B = \forall\alpha.\,(A\to\alpha)\to(B\to\alpha)\to\alpha.
• 𝖫𝗂𝗌𝗍A=∀α.(A→α→α)→α→α\mathsf{List}\,A = \forall\alpha.\,(A\to\alpha\to\alpha)\to\alpha\to\alpha.5 Metatheory: Type Safety and Strong Normalization
5.1 Type Safety
• Preservation and Progress hold in System F by standard proofs (TAPL §15).
• No stuck well‐typed terms, including type‐applications.5.2 Strong Normalization
• Every well‐typed term in System F is strongly normalizing (Girard’s theorem).
• Consequence: no general recursion can be typed in System F.6 Parametricity and Free Theorems
6.1 Reynolds’s Abstraction Theorem
For each closed term M:τM:\tau there is a relational interpretation ⟦τ⟧\llbracket\tau\rrbracket such that (M,M)∈⟦τ⟧(M,M)\in \llbracket\tau\rrbracket. This yields “theorems for free” about the behavior of MM under all instantiations.6.2 Logical Relations
• Define logical relations on types by induction:
– Base types: arbitrary relations.
– Arrow: RA→B(f,g)R_{A\to B}(f,g) iff ∀(x,y)∈RA.(fx,gy)∈RB\forall (x,y)\in R_A.\;(f\,x,g\,y)\in R_B.
– Universal: R∀α.τ(M,N)R_{\forall\alpha.\,\tau}(M,N) iff for all relations SS, (M[A],N[B])∈Rτ[S/α](M\,[A],N\,[B])\in R_{\tau[S/\alpha]}.
• The Fundamental Theorem: well‐typed terms preserve relations.6.3 Examples of Free Theorems
• Any f:∀α.[α]→[α]f:\forall\alpha.\,[\alpha]\to[\alpha] satisfies f[A]∘𝑚𝑎𝑝g=𝑚𝑎𝑝g∘f[B]f\,[A]\circ \mathit{map}_g = \mathit{map}_g\circ f\,[B].
• Any h:∀α.α→α→αh:\forall\alpha.\,\alpha\to\alpha\to\alpha is associative and commutative up to extensional equality (if swapped arguments).7 Beyond System F
7.1 Existential Types for Data Abstraction
Extend types with ∃α.τ\exists\alpha.\,\tau and terms: 𝗉𝖺𝖼𝗄M𝖺𝗌∃α.τ,𝗎𝗇𝗉𝖺𝖼𝗄[α,x]=M𝗂𝗇N \mathsf{pack}\;M\;\mathsf{as}\;\exists\alpha.\,\tau, \quad \mathsf{unpack}\;[\alpha,x]=M\;\mathsf{in}\;N Typing and reduction follow TAPL §15.4.7.2 Bounded Quantification (System F<:)
Allow ∀α<:T.τ\forall\alpha<:T.\,\tau with instantiation restricted by a subtype bound. Typing rules and subtyping (see TP §22).7.3 Type Operators and Kind‐Polymorphism (System Fω)
Introduce types as first‐class:
κ::=*∣κ1→κ2 \kappa ::= * \mid \kappa_1\to\kappa_2 T::=α∣T1T2∣λα:κ.T∣∀α:κ.T T ::= \alpha \mid T_1\;T_2 \mid \lambda\alpha:\kappa.\,T \mid \forall\alpha:\kappa.\,T Enables higher‐kind constructors (e.g.,List,Maybe).7.4 Recursive Types and Iso‐Recursion
System Fωμ or μF combines Fω with fixed‐point operators on types. Supports truly generic data types.8 Practical Let-Polymorphism
8.1 Hindley–Milner Revisited
• Implicit quantification only at let-bindings.
• Principal‐type inference via Algorithm W (Chapter 5).
• ML and Haskell implement variants with type classes or kind‐polymorphism.8.2 Value Restriction and Effects
• In presence of mutable references, only syntactic values may be generalized (value restriction).9 Implementations and Examples
9.1 Haskell GADT Encoding
{-# LANGUAGE RankNTypes #-}
+ - polymorphic identity
id :: forall a. a -> a
id x = x
+ - Church-encoded list
type ListF a = forall r. (a -> r -> r) -> r -> r
nil :: ListF a
nil = \cons nil -> nil
cons :: a -> ListF a -> ListF a
cons x xs = \consF nilF -> consF x (xs consF nilF)- 9.2 OCaml First-Class Modules as Existentials
module type STACK = sig
type t
val empty : t
val push : int -> t -> t
val pop : t -> (int * t)
end
module IntStack : STACK = struct
type t = int list
let empty = []
let push x s = x::s
let pop = function
| x::xs -> (x,xs) | [] -> failwith "empty"
end
let use_stack (module S : STACK) =
let open S in
let s = push 1 empty in
pop s- 10 Chapter Summary
• System F formalizes explicit parametric polymorphism; typable terms enjoy preservation, progress, and strong normalization.
• Many datatypes and operations are encoded uniformly via universal quantification.
• Parametricity yields “free theorems” and justifies data abstraction.
• Extensions (existentials, bounded quantification, higher‐kinds, type operators) enrich expressiveness toward practical languages.
• Let-polymorphism, type inference, and module systems bring polymorphism to everyday programming in ML and Haskell.
In Chapter 8 we will introduce algebraic data types with pattern matching, inductive proofs via structural recursion, and the categorical notion of initial algebras.
- –
In this chapter we move beyond simple and second‐order polymorphic types to fully dependent types, where types may depend on terms. We present the dependent λ–calculus with Π‐types, introduce Σ‐types and identity types, and then build up to the Calculus of Constructions (CoC), which combines dependent types and polymorphism into a single framework. Throughout, we emphasize the propositions-as-types interpretation and the basis for proof assistants such as Coq.
1 Motivation for Dependent Types
• Types indexed by values enable rich specifications:
– Vectors of length nn (𝖵𝖾𝖼An\mathsf{Vec}\;A\;n) rule out out‐of‐bounds errors at the type level.
– Matrices, balanced trees, or sorted lists carry invariants in their types.
• Propositions‐as‐types: logical quantification and proofs become terms in a dependently typed language.
• Dependent types unify data and propositions, computation and proof.2 The Dependent λ-Calculus (λΠ)
2.1 Syntax of Terms and Types
• Sorts: 𝖯𝗋𝗈𝗉\mathsf{Prop} (propositions) and 𝖳𝗒𝗉𝖾\mathsf{Type} (types of computational data).
• Types (and terms) A,B,CA,B,C and terms M,NM,N:
A,B::=x∣𝖯𝗋𝗈𝗉∣𝖳𝗒𝗉𝖾∣Πx:A.B∣λx:A.M∣MN A,B\;::=\; x \mid \mathsf{Prop} \mid \mathsf{Type} \mid \Pi x:A.\,B \mid \lambda x:A.\,M \mid M\;N • A dependent function (Π‐type) Πx:A.B(x)\Pi x:A.\,B(x) generalizes both arrow types (A→BA\to B when BB does not depend on xx) and universal quantification (∀x:A.B(x)\forall x:A.\,B(x) in logic).2.2 Contexts and Judgments
• Context Γ\Gamma is a sequence of bindings x:Ax:A and type‐variable or constant declarations.
• Judgments:
– Γ⊢A:s\Gamma \vdash A : s (type AA has sort s∈{𝖯𝗋𝗈𝗉,𝖳𝗒𝗉𝖾}s\in\{\mathsf{Prop},\mathsf{Type}\})
– Γ⊢M:A\Gamma \vdash M : A (term MM has type AA)
• Conversion rule allows using A≡BA\equiv B up to β‐conversion (and in CoC up to higher universes).2.3 Typing Rules
(Var)
$$ \infer{\Gamma,x:A\vdash x:A}{} $$
(Prod)
$$
\infer{\Gamma\vdash \Pi x:A.\,B : s_2}
{\Gamma\vdash A:s_1
\quad
\Gamma,x:A\vdash B:s_2
\quad
(s_1,s_2)\in\{(\mathsf{Prop},\mathsf{Prop}),(\mathsf{Prop},\mathsf{Type}),(\mathsf{Type},\mathsf{Type})\}}
$$
(Abs)
$$
\infer{\Gamma\vdash \lambda x:A.\,M : \Pi x:A.\,B}
{\Gamma\vdash A:s
\quad
\Gamma,x:A\vdash M:B}
$$
(App)
$$
\infer{\Gamma\vdash M\,N : B[N/x]}
{\Gamma\vdash M:\Pi x:A.\,B
\quad
\Gamma\vdash N:A}
$$
(Sort)
$$
\infer{\Gamma\vdash \mathsf{Prop}:\mathsf{Type}}{}
\quad
\infer{\Gamma\vdash \mathsf{Type}:\mathsf{Type}}{}
$$
(Convert)
$$
\infer{\Gamma\vdash M:B}
{\Gamma\vdash M:A
\quad
\Gamma\vdash A\equiv B}
$$
2.4 Reduction and Conversion
• β‐Reduction: (λx:A.M)N→M[N/x](\lambda x:A.\,M)\,N \to M[N/x].
• Conversion (≡\equiv) is the reflexive‐transitive closure of β‐reduction on types.3 Extensions: Σ‐Types and Identity Types
3.1 Σ–Types (Dependent Pairs)
• Syntax: Σx:A.B(x)\Sigma x:A.\,B(x) is the type of pairs (a,b)(a,b) with a:Aa:A and b:B(a)b:B(a).
• Introduction: 𝗉𝖺𝗂𝗋MN:Σx:A.B(x)\mathsf{pair}\;M\;N : \Sigma x:A.\,B(x).
• Elimination (recursion):
𝖾𝗅𝗂𝗆Σ[x,y]Pzu\mathsf{elim}_{\Sigma}\;[x,y]\,P\;z\;u
projects and feeds components to a continuation.3.2 Identity Types (Equality)
• Syntax: for any A:𝖳𝗒𝗉𝖾A:\mathsf{Type} and x,y:Ax,y:A, 𝖨𝖽A(x,y):𝖳𝗒𝗉𝖾\mathsf{Id}_A(x,y) : \mathsf{Type}.
• Introduction: 𝗋𝖾𝖿𝗅A(x):𝖨𝖽A(x,x)\mathsf{refl}_A(x) : \mathsf{Id}_A(x,x).
• Elimination (J–rule / path induction) gives transport of proofs across equalities.4 The Calculus of Constructions (CoC)
4.1 Combining Polymorphism and Dependent Types
• CoC adds a new sort 𝖳𝗒𝗉𝖾0\mathsf{Type}_0, and allows 𝖳𝗒𝗉𝖾i:𝖳𝗒𝗉𝖾i+1\mathsf{Type}_i : \mathsf{Type}_{i+1} for an infinite hierarchy of universes.
• Polymorphic abstraction Λα:𝖳𝗒𝗉𝖾i.M\Lambda\alpha:\mathsf{Type}_i.\,M and application M[A]M\,[A] are treated as special cases of λ‐abstraction and application at the level of sorts.4.2 Syntax and Rules of CoC
• Sorts s::=𝖯𝗋𝗈𝗉∣𝖳𝗒𝗉𝖾0∣𝖳𝗒𝗉𝖾1∣⋯s ::= \mathsf{Prop} \mid \mathsf{Type}_0 \mid \mathsf{Type}_1\mid\cdots
• Extended Prod rule allows (s1,s2)∈{(𝖯𝗋𝗈𝗉,𝖯𝗋𝗈𝗉),(𝖯𝗋𝗈𝗉,𝖳𝗒𝗉𝖾i),(𝖳𝗒𝗉𝖾i,𝖳𝗒𝗉𝖾i)}(s_1,s_2)\in\{(\mathsf{Prop},\mathsf{Prop}),(\mathsf{Prop},\mathsf{Type}_i),(\mathsf{Type}_i,\mathsf{Type}_i)\}, and polymorphic Prod (𝖳𝗒𝗉𝖾i,𝖳𝗒𝗉𝖾i+1)(\mathsf{Type}_i,\mathsf{Type}_{i+1}).
• All other rules (Var, Abs, App, Convert) carry over.4.3 Curry–Howard: Propositions as Types
• Type Πx:A.B(x)\Pi x:A.\,B(x) corresponds to ∀x:A.B(x)\forall x:A.\,B(x).
• Implication A→BA\to B is Π_:A.B\Pi\_:A.\,B.
• Conjunctions and disjunctions emerge from Σ‐types and tagged sums.
• Proof terms are inhabitants of proposition‐types.5 Examples in CoC
5.1 Natural Numbers and Induction
In CoC with an inductive extension (Calculus of Inductive Constructions, CIC) one declares
Inductive nat : Type_0 :=
| O : nat
| S : nat → nat.and obtains the induction principle 𝗇𝖺𝗍_𝗋𝖾𝖼𝗍:ΠP:𝗇𝖺𝗍→𝖳𝗒𝗉𝖾.PO→(Πn:𝗇𝖺𝗍.Pn→P(Sn))→Πn.Pn. \mathsf{nat\_rect} : \Pi P:\mathsf{nat}\to\mathsf{Type}.\; P\,O \to (\Pi n:\mathsf{nat}.\,P\,n\to P\,(S\,n))\to \Pi n.\,P\,n.
- 5.2 Vectors Indexed by Length
Inductive vec (A:Type_0) : nat → Type_0 :=
| vnil : vec A O
| vcons : Π n:nat, A → vec A n → vec A (S n).This encoding guarantees that vhead applied only to
non‐empty vectors:
Definition vhead {A n} (v: vec A (S n)) : A :=
match v with vcons _ x _ _ => x end.6 Metatheory of CoC
6.1 Subject Reduction and Confluence
• Reduction is confluent; type assignments are preserved under β‐reduction.
• Conversion uses β‐equivalence, and Convert rule ensures well‐typedness is stable.6.2 Strong Normalization and Consistency
• CoC is strongly normalizing: no infinite reduction sequences for well‐typed terms.
• Consistency: there is no term of type 𝖯𝗋𝗈𝗉→𝖳𝗒𝗉𝖾0\mathsf{Prop} \to \mathsf{Type}_0 proving false propositions.7 Dependent Pattern Matching and Inductive Families
7.1 General Inductive Types
• Inductive families generalize Σ‐ and identity types to arbitrary constructors indexed by parameters and indices.
• Eliminators (recursors and inductive predicates) derive from type‐theoretic principles.7.2 Proof by Dependent Elimination
• Pattern match on an inductive proof to derive new proofs.
• Tactics in proof assistants orchestrate these eliminations automatically.8 Practical Systems: Coq and Agda
8.1 Coq’s Calculus of Inductive Constructions
• Universe polymorphism, modules, notations, coercions, proof tactics.
• Kernel: small trusted core performing type‐checking and reduction.8.2 Agda
• Interactive programming with dependent types, mixfix operators, totality checking.
• Emphasis on equational style and user-defined inductive families.9 Chapter Summary
• Dependent types generalize simple and polymorphic types: Π\Pi‐types serve both as function spaces and universal quantification.
• Σ‐types capture dependent pairs and logical existential quantification; identity types represent propositional equality.
• The Calculus of Constructions unifies polymorphism and dependency with a hierarchy of universes.
• Curry–Howard identifies proofs with terms; induction and pattern matching arise from inductive definitions.
• Coq and Agda implement these theories, enabling interactive proof development and dependently typed programming.
In Chapter 9 we will study inductive and coinductive types in depth, covering structural and coinductive recursion, observational type theory, and applications to streams and reactive systems.
- –
In this chapter we present the remarkable correspondence between
proofs in (intuitionistic) logic and well‐typed terms in a λ‐calculus.
Under the Curry–Howard isomorphism (also “propositions‐as‐types” or
“formulas‐as‐types”),
• propositions ↔︎ types
• proofs ↔︎ programs
• proof normalization (cut–elimination) ↔︎ term reduction
We begin with propositional logic and the simply‐typed λ‐calculus with
products, sums, unit and void, then extend to second‐order and dependent
logics, sketch the categorical semantics, and conclude with classical
extensions and applications to proof assistants.
1 Propositional Logic and λ‐Calculus
1.1 Syntax of Propositional Formulas
$$ φ,\;ψ ::= P \mid φ\toψ \mid φ\landψ \mid φ\lorψ \mid ⊤ \mid ⊥ $$ where PP ranges over propositional atoms.1.2 Natural‐Deduction Rules
– Implication
• (→\to‐I) From Γ,φ⊢ψ\Gamma,φ⊢ψ infer$\Gamma⊢φ\toψ$ .
• (→\to‐E) From$\Gamma⊢φ\toψ$ and Γ⊢φ\Gamma⊢φ infer Γ⊢ψ\Gamma⊢ψ.
– Conjunction
• (∧\land‐I) From Γ⊢φ\Gamma⊢φ and Γ⊢ψ\Gamma⊢ψ infer$\Gamma⊢φ\landψ$ .
• (∧\land‐E₁,₂) From$\Gamma⊢φ\landψ$ infer Γ⊢φ\Gamma⊢φ (or Γ⊢ψ\Gamma⊢ψ).
– Disjunction
• (∨\lor‐I₁,₂) From Γ⊢φ\Gamma⊢φ infer$\Gamma⊢φ\lorψ$ (or from Γ⊢ψ\Gamma⊢ψ).
• (∨\lor‐E) From$\Gamma⊢φ\lorψ$ , Γ,φ⊢χ\Gamma,φ⊢χ, and Γ,ψ⊢χ\Gamma,ψ⊢χ infer Γ⊢χ\Gamma⊢χ.
– Truth and False
• (⊤‐I) Γ⊢⊤\Gamma⊢⊤.
• (⊥‐E) From Γ⊢⊥\Gamma⊢⊥ infer Γ⊢φ\Gamma⊢φ for any φφ.1.3 Simply‐Typed λ‐Calculus with Sums and Products
Types
A,B::=α∣A→B∣A×B∣A+B∣1∣0 A,B ::= \alpha \mid A\to B \mid A\times B \mid A+B \mid 1 \mid 0 Terms
M,N::=x∣λx:A.M∣MN∣(M,N)∣𝖿𝗌𝗍M∣𝗌𝗇𝖽M∣𝗂𝗇𝗅M∣𝗂𝗇𝗋M∣𝖼𝖺𝗌𝖾M𝗈𝖿{𝗂𝗇𝗅x→N;𝗂𝗇𝗋y→P}∣()∣𝖺𝖻𝗈𝗋𝗍M M,N ::= x \mid \lambda x:A.\,M \mid M\,N \mid (M,N)\mid \mathsf{fst}\,M\mid\mathsf{snd}\,M \mid \mathsf{inl}\,M\mid\mathsf{inr}\,M\mid \mathsf{case}\;M\;\mathsf{of}\;\{\mathsf{inl}\;x\to N;\,\mathsf{inr}\;y\to P\} \mid () \mid \mathsf{abort}\,M Typing rules mirror the natural‐deduction rules above.2 The Isomorphism: Propositions ≃ Types
2.1 Correspondence Table
•$φ\toψ$ ↔︎ A→BA\to B
•$φ\landψ$ ↔︎ A×BA\times B
•$φ\lorψ$ ↔︎ A+BA+B
• ⊤⊤ ↔︎ 11 (unit type, term ()())
• ⊥⊥ ↔︎ 00 (empty type, no constructors)
• proof rule ↔︎ typing rule2.2 Example: Proof of
$φ\toψ\toφ$
Natural‐deduction derivation
$$ \infer[\to\text{I}] {⊢φ\to(ψ\toφ)} { \infer[\to\text{I}] {φ⊢ψ\toφ} { \infer[\to\text{E}] {φ,ψ⊢φ} {φ⊢φ & φ,ψ⊢ψ} } } $$ Corresponding λ‐term
$$ \lambda x:φ.\,\lambda y:ψ.\,x \quad:\quad φ\to(ψ\toφ) $$3 Second‐Order Logic and System F
3.1 Universal Quantification
Logic: ∀X.φ(X)\forall X.\,φ(X)
Types: ∀α.A(α)\forall α.\,A(α)
Terms: type‐abstraction$\Lambdaα.\,M$ and type‐application M[B]M\,[B].3.2 Example: Polymorphic Identity
– Logic: ⊢∀X.X→X\vdash∀X.\,X\to X.
– System F:
$$ \mathsf{id} = \Lambdaα.\,\lambda x:α.\,x :\;\forallα.\,α\toα $$4 Predicate Logic and Dependent Types
4.1 Universal ∀ and Π‐types
Logic: ∀x:A.P(x)\forall x:A.\,P(x)
Types: Πx:A.P(x)\Pi x:A.\,P(x)4.2 Existential ∃ and Σ‐types
Logic: ∃x:A.P(x)\exists x:A.\,P(x)
Types: Σx:A.P(x)\Sigma x:A.\,P(x)
– witness term a:Aa:A and proof p:P(a)p:P(a) give (a,p):Σx.P(x)(a,p):\Sigma x.\,P(x).5 Cut‐Elimination ↔︎ Normalization
5.1 Cut‐Elimination in Logic
– Removing intermediate lemmas (“cuts”) yields a normal proof.5.2 β‐Reduction in λ‐Calculus
– β\beta‐reducing (λx.M)N(\lambda x.\,M)\,N corresponds to eliminating an implication‐cut.
– Strong normalization ↔︎ every proof normalizes.6 Categorical Semantics: Cartesian and Bicartesian Closed Categories
6.1 CCC for Implicational Logic
– Objects = types/propositions, morphisms = proofs.
– Exponential BAB^A interprets A→BA\to B.
– Terminal object 11 interprets ⊤⊤.6.2 Bicartesian Closed Categories
– Add binary products for ∧\land and coproducts for ∨\lor, initial object 00 for ⊥⊥.
– The Curry–Howard–Lambek correspondence.7 Classical Logic and Control Operators
7.1 Classical Axioms
– Law of excluded middle (φ∨¬φφ\lor¬φ), double‐negation elimination ($¬¬φ\toφ$ ).7.2 Control Constructs in Programming
– Continuation‐passing style (CPS) translation of classical proofs.
– call/cc in Scheme, 𝖼𝖺𝗍𝖼𝗁/𝗍𝗁𝗋𝗈𝗐\mathsf{catch}/\mathsf{throw} as proof terms for ⊥⊥‐elimination.8 Proof Assistants and Program Extraction
8.1 Coq and Agda
– Proofs are terms in CIC; extraction erases proofs to yield executable code.8.2 Examples in Coq
Lemma and_comm (A B : Prop) : A ∧ B → B ∧ A.
Proof. intro p. destruct p as [a b]. split; assumption. Qed.
(* Extracted term:
fun (A B:Type) (p:A*B) =>
match p with (a,b) => (b,a) end
*)- 9 Chapter Summary
• The Curry–Howard correspondence identifies propositions with types
and proofs with programs.
• Natural‐deduction rules for ∧, ∨, →, ⊤, ⊥ correspond exactly to typing
rules for products, sums, functions, unit, and void.
• Second‐order and dependent logics align with System F and
λΠΣ‐calculi.
• Cut‐elimination ↔︎ β‐normalization; strong normalization implies
consistency.
• Bicartesian closed categories provide semantics for propositional
logic.
• Classical logic admits control operators and CPS translations.
• Proof assistants exploit Curry–Howard to build certified programs and
extract executable code.
In Chapter 10 we turn to inductive and coinductive types in depth, exploring structural and coinductive recursion, observational type theory, and applications to infinite data structures and reactive systems.
- –
In this chapter we leave the world of paper‐and‐pen type systems and show how to turn declarative typing rules into concrete algorithms. We cover the classic ML-style inference algorithm W, constraint-based approaches, algorithmic subtyping, bidirectional checking, and practical considerations such as symbol tables, incremental checking, and error reporting. We illustrate with OCaml‐style code.
10.1 The Compiler Front-End: Overview
• Phases
– Lexing & parsing ⇒ Abstract syntax tree (AST)
– Name resolution & scope checking ⇒ annotated AST with unique
identifiers
– Type-checking / type inference ⇒ AST decorated with principal types or
errors
– Desugaring & intermediate representation ⇒ for code generation or
optimization
• Goals of semantic analysis
– Soundness: accept only well‐typed programs (subject‐reduction,
progress)
– Decidability: algorithms terminate on all inputs
– Principal typings: compute most general types where possible
– Good diagnostics: report minimal, actionable error messages
10.2 Name Resolution and Symbol Tables
• Environments
Γ\Gamma
map identifiers to
– Declarations:
𝗏𝖺𝗅x:σ\mathsf{val}\;x:\sigma,
𝖿𝗎𝗇f:(τ→τ′)\mathsf{fun}\;f:(\tau\to\tau'),
– Type‐constructors, modules, record‐fields, etc.
• Scoping rules
– Nesting of
𝗅𝖾𝗍\mathsf{let},
λ\lambda,
𝗆𝗈𝖽𝗎𝗅𝖾\mathsf{module}
⇒ push/pop environments
– Shadowing of names
• Implementation sketch (OCaml pseudo‐code)
type 'a env = (string * 'a) list
let lookup (x:string) (env:'a env) : 'a option =
try Some (List.assoc x env) with Not_found -> None
let extend (x:string) (v:'a) (env:'a env) : 'a env =
(x,v)::env
(* Example: resolve a variable *)
type ty_scheme = Forall of string list * Mono.t
type raw_expr = Var of string | ...
type annotated_expr = Var of int (* De Bruijn or unique id *) | ...
let resolve_names (env:unit env) (e:raw_expr) : annotated_expr = ...10.3 From Declarative to Algorithmic Typing
• Declarative rules (e.g. for STLC, Hindley–Milner) are not directly
executable
• Two main patterns:
– Syntax‐directed checking: every judgment
Γ⊢M:A\Gamma⊢ M : A
corresponds to exactly one rule
– Constraint generation + solving: collect constraints
Ai=BjA_i = B_j
or
Ai<:BjA_i<:B_j
then solve them
• Bidirectional approach: mix checking and inference to support more
features with local annotations
10.4 ML-Style Type Inference: Algorithm W
10.4.1 Preliminaries: Types and Schemes
• Monotypes
τ::=α∣τ→τ∣τ×τ∣1∣0…
τ ::= α \mid τ→τ \mid τ×τ \mid 1 \mid 0\;\dots
• Polytypes (schemes)
σ::=τ∣∀α1…αn.τ
σ ::= τ \mid ∀α_1…α_n.\,τ
• Environments
Γ:x↦σ\Gamma : x ↦ σ
• Instantiation
𝑖𝑛𝑠𝑡(∀α¯.τ)=τ[α¯↦β¯]\,\mathit{inst}(∀\overline α.\,τ) = τ[\overline α ↦ \overline β]\,
(fresh α’s)
• Generalization
𝑔𝑒𝑛(Γ,τ)=∀α∉𝑓𝑣(Γ).τ\,\mathit{gen}(\Gamma,τ)=∀α∉\mathit{fv}(\Gamma).\;τ\,
10.4.2 Unification
• Substitutions
S:α↦τS:α↦τ
extend homomorphically
• Occurs‐check: prevent
α=F(…α…)α = F(…α…)
• Algorithm:
exception Unify_error
let rec unify (t1:Mono.t) (t2:Mono.t) : Subst.t =
match (t1,t2) with
| (Mono.Var α, t) | (t, Mono.Var α) ->
if t = Mono.Var α then Subst.id
else if occurs α t then raise Unify_error
else Subst.singleton α t
| (Mono.Arr(a1,a2), Mono.Arr(b1,b2)) ->
let s1 = unify a1 b1 in
let s2 = unify (Subst.apply s1 a2) (Subst.apply s1 b2) in
Subst.compose s2 s1
| (Mono.Pair(a,b), Mono.Pair(c,d)) ->
let s1 = unify a c in
let s2 = unify (Subst.apply s1 b) (Subst.apply s1 d) in
Subst.compose s2 s1
| (Mono.Unit, Mono.Unit) -> Subst.id
| _ -> raise Unify_error10.4.3 The W Algorithm
(* W : env -> expr -> subst * typ *)
let rec W (env:ty_scheme env) (e:expr) : Subst.t * Mono.t =
match e with
| Var x ->
(match lookup x env with
| None -> error "unbound variable"
| Some σ ->
let τ = instantiate σ in
(Subst.id, τ))
| Lam(x, e1) ->
let α = Mono.fresh_var () in
let env' = extend x (Mono.Var α |> Scheme.of_mono) env in
let (s1, τ1) = W env' e1 in
(s1, Mono.Arr (Subst.apply s1 (Mono.Var α), τ1))
| App(e1,e2) ->
let (s1, τ1) = W env e1 in
let (s2, τ2) = W (Subst.apply_env s1 env) e2 in
let α = Mono.fresh_var () in
let s3 = unify (Subst.apply s2 τ1) (Mono.Arr(τ2, Mono.Var α)) in
(Subst.compose s3 (Subst.compose s2 s1),
Subst.apply s3 (Mono.Var α))
| Let(x,e1,e2) ->
let (s1, τ1) = W env e1 in
let σ = generalize (Subst.apply_env s1 env) τ1 in
let env' = extend x σ (Subst.apply_env s1 env) in
let (s2, τ2) = W env' e2 in
(Subst.compose s2 s1, τ2)
(* plus pairs, sums, unit, etc. *)• Principal Types: W always computes the most general type
• Complexity: roughly
O(n×α(n))O(n×α(n))
per unification; linear in program size for ML
10.5 Constraint-Based Inference and Solving
• Generate a set of equations
C={τi=τj}C = \{τ_i = τ_j\}
or subtyping constraints
τi<:τjτ_i<:τ_j
• Solve via unification or by specialized algorithms (e.g. worklists,
graph algorithms)
• Advantage: decouples AST traversal from solver; easier to extend to
advanced type features
• Example: record subtyping constraints
– $ {l_1:τ_1,…,l_n:τ_n} <: {l_{i_1}:σ_{i_1},…,l_{i_k}:σ_{i_k}}
$
– translate to
τij<:σijτ_{i_j} <: σ_{i_j}
for each field
10.6 Algorithmic Subtyping for F<:
• Declarative rules for
<:<:
can be non‐syntax‐directed because of transitivity
• Algorithmic presentation uses worklist/queue of pending checks
let rec subtype alg_env (t1,t2) =
let worklist = Queue.create () in
Queue.push (t1,t2) worklist;
let rec loop () =
if Queue.is_empty worklist then true else
let (a,b) = Queue.pop worklist in
match (a,b) with
| (TVar x, TVar y) when x=y -> loop ()
| (Arrow(a1,a2), Arrow(b1,b2)) ->
Queue.push (b1,a1) worklist;
Queue.push (a2,b2) worklist;
loop ()
| (Record flds1, Record flds2) when fields_of flds2 ⊆ fields_of flds1 ->
List.iter (fun (l,σ) ->
let τ = List.assoc l flds1 in
Queue.push (τ,σ) worklist) flds2;
loop ()
| (Top, _) -> loop ()
| _ -> false
in loop ()10.7 Bidirectional Type Checking
• Split judgments into
– Synthesis
Γ⊢M⇒τ\Gamma⊢ M ⇒ τ
(infer type of
MM)
– Checking
Γ⊢M⇐τ\Gamma⊢ M ⇐ τ
(verify
MM
has given
ττ)
• Rules ensure at most one applicable per syntax form
• Well suited for systems with GADTs, dependent types, implicit
arguments
10.8 Practical Considerations
10.8.1 Incremental and Modular Checking
• Separate compilation: interface files
(.mli.mli)
store signatures
• Caching of typed ASTs; re‐typechecking only changed modules
10.8.2 Error Reporting and Localization
• Track source positions in AST nodes
• On unification/subtyping failure, record the smallest unsatisfiable
subset of constraints
• Heuristics: hole‐driven diagnostic, blame assignment in gradual
typing
10.9 Putting It All Together: A Mini-OCaml Type Checker
10.9.1 AST Definitions
type mono =
| TVar of string
| TArrow of mono * mono
| TInt
| TBool
| TUnit
type scheme = Forall of string list * mono
type expr =
| Var of string
| Int of int
| Bool of bool
| Lam of string * expr
| App of expr * expr
| Let of string * expr * expr
| If of expr * expr * expr
| Pair of expr * expr
| Fst of expr
| Snd of expr10.9.2 Environment and Substitution
module Subst = struct
type t = (string * mono) list
let id = []
let singleton x τ = [(x,τ)]
let rec apply (s:t) (τ:mono) : mono =
match τ with
| TVar x -> (try List.assoc x s with Not_found -> τ)
| TArrow(a,b) -> TArrow(apply s a, apply s b)
| TInt | TBool | TUnit -> τ
let apply_env s env = List.map (fun (x,sch) ->
(x, instantiate_scheme s sch)) env
let compose s1 s2 =
List.map (fun (x,τ) -> (x, apply s1 τ)) s2 @ s1
end10.9.3 Type Inference Driver
10.10 Chapter Summary
• Semantic analysis orchestrates name resolution, scope checking, and
type validation.
• Algorithm W performs efficient principal-type inference for
Hindley–Milner polymorphism.
• Constraint generation separates AST traversal from solving, easing
extensions.
• Algorithmic subtyping uses worklists to implement declarative rules
without non‐syntax‐directed transitivity.
• Bidirectional checking scales to advanced type systems with local
annotations.
• Practical issues—incrementality, error reporting, modularity—are
crucial for real compilers.
In Chapter 11 we will explore advanced module systems and separate compilation, including ML‐style functors, first-class modules, and the theory of parameterized signatures.
- –
In this chapter we introduce the algebraic foundations of lattices and their central role in both advanced type systems (e.g. intersection/union types, subtype lattices) and in static analysis via abstract interpretation. We develop the theory of partial orders, complete lattices, monotone maps, and fixpoints (Knaster–Tarski, Kleene). Then we present the abstract interpretation framework—Galois connections, soundness, widening/narrowing—and illustrate with concrete OCaml sketches of constant propagation and sign analysis.
11.1 Partial Orders and Lattices
11.1.1 Definitions
• A partial order is a set
(L,≤)(L,≤)
satisfying reflexivity, antisymmetry, transitivity.
• A meet‐semi-lattice has binary meet
⊓\sqcap:
x⊓yx\sqcap y
is greatest lower bound (glb).
• A join‐semi-lattice has binary join
⊔\sqcup:
x⊔yx\sqcup y
is least upper bound (lub).
• A lattice has both
⊓\sqcap
and
⊔\sqcup.
11.1.2 Examples
• Powerset lattice
(𝒫(S),⊆)(\mathcal P(S),⊆)
with
⊓=∩\sqcap=∩,
⊔=∪\sqcup=∪,
bottom
∅∅,
top
SS.
• Integer intervals ordered by inclusion:
[a,b]≤[c,d][a,b] ≤ [c,d]
iff
c≤a∧b≤dc≤a∧b≤d.
• Subtype lattice of record types under width/height subtyping.
11.2 Complete Lattices and Fixpoints
11.2.1 Complete Lattice
•
(L,≤)(L,≤)
is complete if every subset
X⊆LX⊆L
has
⨆X\bigsqcup X
and
⨅X\bigsqcap X.
• In particular, bottom
⊥=⨆∅\bot=\bigsqcup∅,
top
⊤=⨅∅\top=\bigsqcap∅.
11.2.2 Knaster–Tarski Theorem
Theorem. If
f:L→Lf:L→L
is monotone on a complete lattice, then its set of fixpoints forms a
complete lattice. In particular,
𝑙𝑓𝑝(f)=⨅{x∈L∣f(x)≤x},𝑔𝑓𝑝(f)=⨆{x∈L∣x≤f(x)}.
\mathit{lfp}(f)=\bigsqcap\{\,x∈L\mid f(x)≤x\}\;,\quad
\mathit{gfp}(f)=\bigsqcup\{\,x∈L\mid x≤f(x)\}.
11.3 Monotone Functions and Kleene’s Fixpoint Theorem
• A function
f:L→Lf:L→L
is monotone if
x≤y⇒f(x)≤f(y)x≤y⇒f(x)≤f(y).
• If
LL
is a chain‐complete poset and
ff
is continuous (preserves lub of ω‐chains), then
𝑙𝑓𝑝(f)=⨆n=0∞fn(⊥).
\mathit{lfp}(f)=\bigsqcup_{n=0}^\infty f^n(\bot).
• This yields the standard
iterative fixpoint algorithm.
11.4 Lattices in Type Systems
11.4.1 Intersection Types
• Types
A∧BA∧B
denote values at both
AA
and
BB.
•
(𝒯,≤)(\mathcal T,≤)
with
≤≤
as subtype relation extended by
A∧B≤AA∧B≤A,
A∧B≤BA∧B≤B,
and if
C≤AC≤A
and
C≤BC≤B
then
C≤A∧BC≤A∧B.
• Meet
⊓\sqcap
is
∧∧,
join
⊔\sqcup
is least common supertype (if exists).
11.4.2 Union Types
•
A∨BA∨B
denotes values at either
AA
or
BB.
• Join
⊔\sqcup
is
∨∨,
meet is greatest common subtype (often approximate).
11.4.3 Subtype Lattices
• Many type systems form bounded lattices: top
⊤⊤
(dynamic or any), bottom
⊥⊥
(uninhabited).
• Fields‐record subtyping and arrow‐covariance/contravariance form
partial orders with meets/joins.
11.5 Abstract Interpretation Framework
11.5.1 Galois Connections and Insertions
A Galois connection between concrete domain
(C,≤C)(C,≤_C)
and abstract domain
(A,≤A)(A,≤_A)
is a pair
(α:C→A,γ:A→C)(α:C→A,\,γ:A→C)
such that
∀c∈C,∀a∈A.α(c)≤Aa⇔c≤Cγ(a).
∀c∈C,\;∀a∈A.\quad α(c)≤_A a \iff c≤_C γ(a).
If additionally
α∘γ=𝑖𝑑Aα∘γ= \mathit{id}_A,
it is a Galois insertion.
11.5.2 Abstraction and Concretization
•
αα
over‐approximates concrete sets;
γγ
maps abstract elements back to concrete semantics.
• To analyze a concrete semantic function
f:C→Cf:C→C,
define
f♯=α∘f∘γ:A→Af^♯=α∘f∘γ : A→A.
• Soundness:
α(f(c))≤Af♯(α(c))α(f(c)) ≤_A f^♯(α(c))
for all
cc.
11.6 Common Abstract Domains
11.6.1 Sign Domain
Domain
Asign={⊥,A_{sign}=\{\bot,\,Neg,Zero,Pos,NegZero,ZeroPos,NegPos,Top}\}.
Ordering by information:
e.g. ⊥≤\bot≤Neg≤Top.
Join and meet tables are finite.
11.6.2 Interval Domain
Elements are intervals
[a,b][a,b]
with
a∈ℤ∪{−∞}a∈\mathbb Z∪\{-∞\},
b∈ℤ∪{+∞}b∈\mathbb Z∪\{+∞\}
and
a≤ba≤b.
Join is convex hull, meet is intersection (or widened intersection).
11.6.3 Reduced Product
Combination of domains
A×BA\times B
quotiented to remove infeasible pairs, improving precision.
11.7 Fixpoint Computation Strategies
11.7.1 Kleene Iteration
Compute ascending chain
⊥,f(⊥),f2(⊥),…⊥,f(⊥),f^2(⊥),…
until stabilization.
11.7.2 Worklist (Chaotic) Iteration
• Maintain a queue of program points whose abstract state may
change.
• Recompute successors until no change.
11.7.3 Widening and Narrowing
• Widening
▽▽
forces chains to stabilize:
xn+1=xn▽f(xn)x_{n+1}=x_n▽f(x_n).
• Narrowing
△△
recovers precision: descending iteration starting from post‐widen
fixpoint.
11.8 Implementation Sketch: A Mini Abstract Interpreter (OCaml)
11.8.1 Syntax of a Tiny Imp Language
type var = string
type expr =
| Const of int
| Var of var
| Add of expr * expr
type stmt =
| Assign of var * expr
| Seq of stmt * stmt
| If of expr * stmt * stmt
| While of expr * stmt11.8.2 Sign Domain Representation
type sign = Bot | Neg | Zero | Pos | Top
let leq a b =
match (a,b) with
| (Bot,_) -> true
| (_,Top) -> true
| (Neg,Neg)|(Zero,Zero)|(Pos,Pos) -> true
| _ -> false
let join a b =
match (a,b) with
| (Bot,x)|(x,Bot) -> x
| (Neg,Pos)|(Pos,Neg) -> Top
| (x,y) when x=y -> x
| _ -> Top
let const_sign n =
if n<0 then Neg else if n>0 then Pos else Zero11.8.3 Abstract Evaluation
type abs_state = (var * sign) list
let lookup x st =
try List.assoc x st with Not_found -> Bot
let eval_expr st = function
| Const n -> const_sign n
| Var x -> lookup x st
| Add(e1,e2) ->
join (eval_expr st e1) (eval_expr st e2)11.8.4 Fixpoint Engine with Worklist and Widening
let analyze (prog:stmt) : abs_state =
let states = Hashtbl.create 16 in
let work = Queue.create () in
(* init entry state *)
Hashtbl.add states 0 []; Queue.push 0 work;
while not (Queue.is_empty work) do
let pc = Queue.pop work in
let st = Hashtbl.find states pc in
let st' = transfer prog st in
let prev = Hashtbl.find states (succ pc) in
let joined = join_states prev st' in
let widened = if leq joined prev then prev else join prev joined in
if not (leq widened prev) then begin
Hashtbl.replace states (succ pc) widened;
Queue.push (succ pc) work
end
done;
Hashtbl.find states (final_pc prog)11.9 Case Study: Constant Propagation
• Abstract domain: lattice of constants plus “unknown”
⊤\top.
• Transfer: propagate known constants through expressions; join at
merges.
• Enables dead‐code elimination and strength reduction.
11.10 Case Study: Sign Analysis
• As above, tracks sign of integer variables.
• Widen intervals to ensure termination on loops.
11.11 Summary
• Lattices and complete lattices provide the algebraic backbone for both
subtype/intersection‐union type systems and abstract domains in static
analysis.
• Knaster–Tarski and Kleene fixpoint theorems guarantee existence and
computability of fixpoints for monotone/continuous maps.
• Galois connections formalize sound abstractions; widening/narrowing
enforce termination and precision trade‐offs.
• Worklist algorithms and OCaml sketches show how to build a minimal
abstract interpreter for constant propagation and sign analysis.
In Chapter 12 we’ll explore effect systems and monadic semantics, showing how to track and control side effects in typed functional languages.
- –
In this chapter we survey the rich landscape of type‐system features as they appear in modern functional programming languages. We begin with the classic Hindley–Milner system of ML‐languages, extend it with algebraic data types and pattern matching, then move to Haskell’s powerful type‐class mechanism, GADTs, higher‐rank and higher‐kinded polymorphism, and ML‐style modules and functors. We conclude with a look at type‐level programming (type families, data kinds) and practical inference strategies and error reporting.
12.1 Hindley–Milner Polymorphism Revisited
12.1.1 Syntax and Declarative Typing
• Expressions
– Variables:
xx
– Abstraction:
λx.e\lambda x.\,e
– Application:
e1e2e_1\,e_2
– Let‐binding:
𝗅𝖾𝗍x=e1𝗂𝗇e2\mathsf{let}\;x = e_1\;\mathsf{in}\;e_2
• Types
τ::=α∣τ1→τ2
\tau ::= α \mid τ_1 \to τ_2
• Typing rules Gen, Inst, Abs, App, Let (as in Chapter 10).
12.1.2 Principal Types and Inference (Algorithm W)
• Recall principal type property: every typable expression has a most
general type
σσ
such that any other instance is an instantiation of
σσ.
• Algorithm W from Section 10.4 infers principal types in
O(nα(n))O(n\,α(n))
time.
12.1.3 Value Restriction in OCaml
• Mutable references break unrestricted generalization.
• OCaml enforces the value restriction: only syntactic values may be
generalized in a
𝗅𝖾𝗍\mathsf{let}.
12.2 Algebraic Data Types and Pattern Matching
12.2.1 Definition of ADTs
• Sum‐of‐products types:
type ’a list = Nil | Cons of ’a * ’a list ```
• Constructors
Ci:τi↦Dτ¯C_i : τ_i ↦ D\;\overline{τ}.
12.2.2 Typing Rules for Constructors and Case
– Constructor rule:
Γ⊢ei:τiΓ⊢C(e1,…,en):Dτ1⋯τn
\Gamma⊢e_i:τ_i \quad
\Gamma⊢C(e_1,\dots,e_n):D\;τ_1\cdots τ_n
– Case analysis:
$$
\infer
{ \Gamma⊢e:D\;\overline{τ}
\quad\forall
i.\;\Gamma,x_{i1}:τ_{i1},\dots,x_{ik_i}:τ_{ik_i}⊢e_i:τ }
{
\Gamma⊢\mathsf{match}\;e\;\mathsf{with}\;C_i(\overline{x_i})\to e_i : τ
}
$$
12.2.3 Type Inference for ADTs
• ADTs do not affect principal‐type inference: constructors are treated
as polymorphic constants.
• Pattern‐match coverage and exhaustiveness checking ensure runtime
safety.
12.3 Type Classes and Overloading (Haskell)
12.3.1 Class and Instance Declarations
• Class:
class Eq α where (==) :: α→α→Bool
• Instance:
instance Eq Int where x == y = x `intEq` y
12.3.2 Dictionary Passing Semantics
• Desugar each
(==)(==)-call
to passing a record of function pointers (the “dictionary”).
• At
𝖿x\mathsf{f}\;x
with
𝖿::∀α.Eqα⇒α→α→Bool\mathsf{f} :: \forall α. Eq\;α ⇒ α→α→Bool,
inference produces:
(d:𝐸𝑞𝐷𝑖𝑐𝑡τ),x:τ⊢d.(==)x
(d:\mathit{EqDict}\;τ),\;x:τ⊢d.(==)\;x
12.3.3 Functional Dependencies and Multi‐Parameter Classes
• Allow declarations like
class Convertible α β | α → β where convert :: α→β
• FD
α→βα→β
enforces at most one
ββ
per
αα.
12.3.4 Defaulting and coherence rules
12.4 Generalized Algebraic Data Types (GADTs)
12.4.1 Syntax
data Expr a where LitInt :: Int → Expr Int LitBool :: Bool → Expr Bool Add :: Expr Int → Expr Int → Expr Int If :: Expr Bool → Expr a → Expr a → Expr a
12.4.2 Typing
• Each constructor refines the result type
aa
in the context of the match.
• Typing rule for GADT‐case:
$$
\infer
{ \Gamma⊢e:Expr\,τ
\quad\forall C_i.\;C_i:\overline{σ_i}→Expr\,τ_i
\quad \Gamma,\overline{x_i:σ_i}⊢e_i:ρ }
{
Γ⊢\mathsf{case}\;e\;\mathsf{of}\;\dots\;C_i(\overline{x_i})→e_i : ρ }
$$
12.4.3 Inference Challenges
• Type‐directed elaboration or bidirectional checking is required for
principal typing.
12.5 Module Systems: ML‐Style Modules and Functors
12.5.1 Signatures
signature STACK = sig type 'a t val empty : 'a t val push : 'a → 'a t → 'a t val pop : 'a t → ('a * 'a t) option end
12.5.2 Structures and Functors
``` structure ListStack : STACK = struct type ’a t = ’a list let empty =
[] let push x s = x::s let pop = function []→None | x::xs→Some(x,xs)
end
functor MakeLoggingStack(X:STACK) = struct
include X
let push x s =
print_endline "push";
X.push x s
end
``` 12.5.3 Type Sharing and Abstraction
• sharing type constraints enforce equal abstract types
across signatures.
• Functor application type‐checks by signature matching and optionally
volatile type generativity.
12.6 Advanced Polymorphism
12.6.1 Higher‐Kinded Types
• Kind system:
*∣*→*∣(*→*)→**\mid *→* \mid (*→*)→*
…
• Monad :: (*→*)→* class Monad m where …
12.6.2 Rank‐N Types
• Haskell syntax:
f :: (∀α. α→α) → Int
• Requires explicit type annotations and bidirectional checking.
12.6.3 Row Polymorphism (Extensible Records/Variants)
• Types of the form { l_i:τ_i | ρ } with row variable
ρρ.
• Enables polymorphic functions over records that may have extra
fields.
12.7 Type‐Level Programming and Dependent‐Lite Features
12.7.1 Data Kinds and Kind Promotion
data Nat = Z | S Nat data Vec :: Nat → * → * where VNil :: Vec Z a VCons :: a → Vec n a → Vec (S n) a
12.7.2 Type Families and Functional Dependencies
type family F a b :: * type instance F Int Bool = Char
12.7.3 Implicit Arguments and Dependent Patterns (Agda/Idris style)
12.8 Implementation and Inference in Practice
12.8.1 Bidirectional Type Checking
• Split judgments: inference (⇒) vs. checking
(⇐).
• Ensures decidability in presence of higher‐rank and GADTs.
12.8.2 Constraint Solving and Solver Plugins
• Class constraints solved by dictionary‐generation.
• GHC plugins may customize unification and constraint rewriting.
12.8.3 Error Reporting and Type Debugging
• Source‐span tracking for better diagnostics.
• Techniques: hole‐driven refinement, deferred constraint
collection.
12.9 Chapter Summary
• ML‐style Hindley–Milner gives principled let‐polymorphism with
efficient inference.
• Algebraic data types and pattern matching introduce sum‐and‐product
types naturally.
• Haskell’s type classes provide ad‐hoc polymorphism via dictionary
passing.
• GADTs and higher‐rank polymorphism push the boundary toward dependent
types and require bidirectional checking.
• Module systems support large‐scale program structuring with abstract
types and parameterization.
• Advanced features—higher kinds, row polymorphism, type‐level
programming—enable expressive, correct-by‐construction code.
• In practice, bidirectional checking, constraint solving, and improved
error messages make sophisticated type systems tractable in real
compilers.
- –
In this chapter we survey how typing disciplines adapt to non-functional paradigms: class-based object-oriented languages, logic programming languages, and imperative languages with mutable state. We study their core calculi, typing rules, inference challenges, subtyping, generics, effects, ownership, and typestate.
13.1 Object-Oriented Type Systems
13.1.1 Core Calculus: F<: and Featherweight Java
• Syntax (classes, fields, methods):
L ::= C extends D { f; K; M }
K ::= C(x f) { super(x); this.f = x; }
M ::= T m(T x){ return e; }
e ::= x | e.f | e.m(e) | new C(e) | (T) e
```
• Nominal subtyping:
C<:DC<:D
iff
CC
extends
DD
(transitively).
• Typing rules (select, invoke, new, cast) mirror STLC but with
subtyping:
– T-NEW: if
fields(C)=Tififields(C) = T_i\,f_i
and
Γ⊢ei:Ui\Gamma⊢e_i:U_i
with
Ui<:TiU_i<:T_i,
then
Γ⊢𝗇𝖾𝗐C(ei):C\Gamma⊢\mathsf{new}\;C(e_i):C.
– T-INVK: if
Γ⊢e0:C0\Gamma⊢e_0:C_0
and
mtype(m,C0)=T¯→Tmtype(m,C_0) = \overline{T}\to T,
and
Γ⊢ei:Ui\Gamma⊢e_i:U_i
with
Ui<:TiU_i<:T_i,
then
Γ⊢e0.m(e):T\Gamma⊢e_0.m(e):T.
– T-SUB and T-CAST handle explicit upcasts/downcasts.
• Safety: Preservation + Progress hold in Featherweight Java.
13.1.2 Generics and Variance (Java/C#)
• Generic class declaration:
class C<X extends B> { … }.
• Erasure vs. reification: Java erases type parameters at runtime; C#
reifies.
• Variance annotations:
– Java wildcards: List<? extends T> (covariant),
List<? super T> (contravariant).
– C# out T (covariant), in T
(contravariant).
• Sound typing: subtyping on parameterized types follows
declaration-site variance or use-site wildcards.
• Example:
interface ReadOnlyList<out T> { T get(int i); } ReadOnlyList<Animal> animals = new ReadOnlyList<Dog>();
13.1.3 Path-Dependent and Structural Generics (Scala)
• Path-dependent types:
trait Container { type Elem; def get: Elem } def head(c: Container): c.Elem = c.get
• Structural typing via refinement:
type Sized = { def size: Int } def f(x: Sized) = x.size
• F-bounded polymorphism: class C[X <: C[X]] enables
self types.
13.1.4 Dependent Object Types (DOT)
• Merge nominal and dependent types: x.T is a type
selection.
• Syntax:
p ::= x | p.l T ::= { type L: S..U; val l: T } | p.L | T & T | T ∨ T | Top | Bot
• Typing judgments track refinement and recursive object types.
• Used to model Scala’s full type system.
13.2 Logic-Oriented Type Systems
13.2.1 Untyped vs. Typed Logic Programming
• Prolog has no static types; errors surface at runtime.
• Typed logic languages: Mercury, Gödel, λProlog introduce static type
checking.
• Simple Hindley–Milner style for Horn clauses:
Clause : A ← B₁,…,B_n Atom : p(t₁,…,t_k)
with declared types for predicates
p : τ₁×…×τ_k → Bool.
• Type‐checking ensures each p(t₁,…,t_k) has
ti:τit_i:τ_i.
13.2.2 Mode and Determinism Typing (Mercury)
• Modes (in, out) annotate argument usage:
:- mode foo(in, out) is det.
• Compiler checks that in arguments are ground on call and
out are fresh on return.
• Determinism categories (det, semidet,
multi, nondet) form a lattice to track success
count.
13.2.3 Higher-Order and λProlog
• λProlog extends Horn clauses with simply‐typed λ-terms and
higher-order unification.
• Types:
τ::=α∣τ→ττ ::= α \mid τ→τ.
• Clauses and goals typed under this calculus; allows predicates as
first‐class values.
13.2.4 Constraint Logic Programming (CLP)
•
CLP(DD)
integrates a domain
DD
(e.g. finite‐domains, reals) as an abstract lattice.
• Types and constraints align: unification becomes constraint solving in
DD.
• Soundness: typed CLP ensures all constraint calls respect domain
operation signatures.
13.3 Imperative Language Type Systems
13.3.1 STLC with References
• Extend STLC with mutable cells:
τ::=…∣𝖱𝖾𝖿τ
τ ::= … \mid \mathsf{Ref}\;τ
e::=…∣𝗋𝖾𝖿e∣!e∣e:=e
e ::= … \mid \mathsf{ref}\;e \mid !e \mid e:=e
• Typing rules:
– T-REF: if
Γ⊢e:τ\Gamma⊢e:τ
then
Γ⊢𝗋𝖾𝖿e:𝖱𝖾𝖿τ\Gamma⊢\mathsf{ref}\;e:\mathsf{Ref}\;τ.
– T-DEREF: if
Γ⊢e:𝖱𝖾𝖿τ\Gamma⊢e:\mathsf{Ref}\;τ
then
Γ⊢!e:τ\Gamma⊢!e:τ.
– T-ASSIGN: if
Γ⊢e1:𝖱𝖾𝖿τ\Gamma⊢e_1:\mathsf{Ref}\;τ
and
Γ⊢e2:τ\Gamma⊢e_2:τ
then
• Store typing judgment
Σ⊢μ\Sigma⊢\mu
tracks heap cells.
• Preservation and Progress hold in the presence of a well‐typed
store.
13.3.2 Effect Systems
• Annotate expressions with effect sets
εε
(e.g. {𝗋𝖾𝖺𝖽,𝗐𝗋𝗂𝗍𝖾}\{\mathsf{read},\mathsf{write}\}).
• Judgment:
Γ⊢e:τ!ε\Gamma⊢ e : τ \;!\;ε.
• Compose effects:
$$
\infer
{Γ⊢ e_1:τ_1\!ε_1 \quad Γ,x:τ_1⊢ e_2:τ_2\!ε_2}
{Γ⊢\mathsf{let}\;x=e_1\;\mathsf{in}\;e_2 : τ_2\!ε_1∪ε_2}
$$
• Enables static tracking of stateful operations, I/O, exceptions.
13.3.3 Region and Ownership Types
• Regions group allocated storage to enforce lifetimes and prevent
dangling pointers.
• Ownership types (e.g. in Cyclone, Rust) track aliasing and mutation
privileges:
– In Rust: &T (shared borrow), &mut T
(unique borrow).
– Borrow checker enforces no mutable aliasing and lifetime scopes.
• Typestate (linear types) ensure protocols: e.g. file handles must be
opened before read, closed after.
13.3.4 Mutable Object-Oriented Imperative Languages (Java/C)
• Java’s type system enforces memory safety (no pointer arithmetic),
null‐checks deferred to runtime.
• C’s nominal types are unsound under casts and pointer
arithmetic.
• Refinement types (Liquid Haskell, F*) add logical predicates
τ{x∣p(x)}τ\,\{x\mid p(x)\}
to guarantee array bounds, non-null, arithmetic invariants.
13.4 Combining Paradigms: Multiparadigm Languages
• Scala, F#, Kotlin integrate functional, OOP, imperative style under a
unified type system (DOT in Scala, ML-style in F#).
• Hybrid features: async effects, algebraic effects, dependent typing
fragments.
13.5 Chapter Summary
• Object-oriented type systems rest on nominal subtyping, generics,
variance, and core calculi (F<:, Featherweight Java).
• Logic languages gain safety via simple Hindley–Milner typing, modes,
determinism, and higher-order types.
• Imperative typing extends STLC with references, effects, regions,
ownership, and refinement to ensure memory and protocol safety.
• Multiparadigm languages combine these techniques, showing the
versatility of modern type‐system design.
- –
In this final chapter we survey the state of the art in automated and semi-automated typing techniques—how types are inferred, how static and dynamic typing can coexist, and which research directions lie ahead.
14.1 Foundations of Type Inference
14.1.1 Hindley–Milner and Algorithm W
• Recall types
τ::=α∣τ1→τ2
τ ::= α \mid τ_1 → τ_2
and schemes
σ::=∀α¯.τ.
σ ::= ∀\,\overline{α}. τ.
• Algorithm W:
– Traverses the AST, generates fresh type variables
αiα_i.
– Emits unification constraints
τ1=τ2τ_1 = τ_2.
– Solves by union-find in nearly linear time
O(nα(n))O(n α(n)).
• Principal typing: every expression has a most general type;
instantiation yields all others.
14.1.2 Constraint-Based and Baader–Siek Variants
• Instead of immediate unification, collect constraints
C::=τ1≡τ2∣C∧C
C ::= τ_1 ≡ τ_2 \mid C∧C
and solve in batch.
• Enables richer features (row polymorphism, type classes) by
generalizing equality to other relations
(e.g. ≤≤
for subtyping).
• Baader–Siek local inference: infer as much as possible, ask user for
top-level annotations when needed.
14.1.3 Local vs. Global Inference
• ML–style inference is global within a module boundary: all definitions
in scope influence each other.
• Local inference (e.g. Scala, Kotlin) requires user annotations at
method boundaries; improves compile times and modularity.
• Trade-off: precision vs. predictability vs. performance.
14.2 Bidirectional Type Checking
• Split judgments:
– Synthesis (inference)
Γ⊢e⇒τ\Gamma⊢ e ⇒ τ
– Checking (verification)
Γ⊢e⇐τ\Gamma⊢ e ⇐ τ
• Rules direct the flow of information: annotations drive checking,
while simple constructs synthesize.
• Essential for features that break principal typing:
– Higher-rank polymorphism
(∀∀
inside arguments)
– GADTs (type‐refinement in pattern matches)
– Implicit/coercion resolution (type classes, implicits).
14.3 Inference for Advanced Type Features
14.3.1 GADTs and Existentials
• GADT constructors carry extra equalities:
data Expr a where LitInt :: Int → Expr Int If :: Expr Bool → Expr a →
Expr a → Expr a
``• Unification must record and solve equalities $a ≡ Int$ in the branch whereLitInt`
applies.
• Full inference is undecidable—bidirectional checking or local
annotations are used.
14.3.2 Type Classes, Traits and Implicits
• Constraint generation: each usage of a class method emits a constraint
EqτEq τ.
• Dictionary‐passing semantics at compile time; instance search reduces
to satisfiability in a Horn‐clause database.
• Overlapping/undecidable instances require user annotations or
pragmas.
14.3.3 Modular and Higher-Module Inference
• Functor and module systems obstruct classical inference: abstract
types block unification across module boundaries.
• Solutions:
– Constraint packaging: carry module constraints in signatures.
– Partial inference inside modules; require user‐written signatures.
14.4 Gradual Typing
14.4.1 The Unknown Type and Consistency Relation
• Introduce the unknown type ? into the type grammar:
τ::=…∣?
τ ::= … \mid \,?
• Consistency
τ∼στ ∼ σ
is a reflexive, symmetric relation that treats ? as
consistent with every type.
• Static check: allow τ ∼ σ; dynamic semantics: insert
casts to check at runtime.
14.4.2 Cast Insertion and Blame Calculus
• During elaboration, each implicit conversion between
ττ
and
σσ
(where
τ∼στ ∼ σ)
is translated to
⟨σ ⇐ τ⟩ e
a runtime check.
• Blame labels track which side (static or dynamic) is responsible for a
type violation.
• Guarantees: “well-typed programs cannot be blamed on the static
side.”
14.4.3 Implementations and Trade-Offs
• Racket: contracts as first-class, gradual by design.
• TypeScript/Dart/MyPy: gradual typing in mainstream JS/Python
platforms; unsoundness accepted for interoperability.
• Performance: runtime casts incur overhead; optimizing cast‐elimination
is an active area.
14.5 Refinement and Liquid Type Inference
14.5.1 Refinement Types and Predicates
• Types of the form
{x:τ∣p(x)}
\{\,x:τ\mid p(x)\}
where
p(x)p(x)
is a logical predicate
(e.g. 0≤x<𝗅𝖾𝗇(𝑎𝑟𝑟)0 ≤ x < \mathsf{len}(\mathit{arr})).
• Verification reduces to checking predicate implications via SMT
solvers.
14.5.2 Liquid Types
• Restrict refinements to conjunctions of qualifiers drawn from a finite
template set.
• Inference:
– Generate logical Horn constraints
p⇒qp⇒q
from program semantics.
– Solve using predicate abstraction and fixpoint iteration.
• Systems: Liquid Haskell, F★, Dafny.
14.5.3 Precision vs. Automation
• More expressive predicates → more solver burden.
• User‐supplied “hints” or refinement annotations guide the
inference.
14.6 Emerging Research Directions
• Effect Inference and Algebraic Effects
– Automatic inference of effect rows
εε
in
τ→τ′!ετ→τ′ ! ε.
• Quantitative and Probabilistic Types
– Track resource usage, termination probabilities.
• Gradual Dependent Typing
– Marry full dependent types
(ΠΠ‐types)
with gradual casts and blame.
• Typed Meta-Programming and Macros
– Ensure hygiene and type safety in code generation (e.g. Typed Template
Haskell).
• Cross-Language Type Interoperability
– Gradual and semantic types as a lingua franca for multi-language
systems.
14.7 Challenges and Opportunities
• Better Error Reporting and Repair
– ML-based suggestions, interactive type debugging, root‐cause
localization.
• Machine-Learning Guided Inference
– Predict missing annotations, select instances, guide solver
strategies.
• Formalization and Mechanized Metatheory
– Scalable proof frameworks (e.g. Ott, Coq, Lean) for richer
calculi.
• Towards Ubiquitous, Principled Typing
– Seamless blend of static/dynamic, modular, effectful, dependent
features—bringing proof-power to mainstream programming.
14.8 Chapter Summary
• Type inference has evolved from pure HM/Algorithm W to
constraint-based, bidirectional, and solver-aided approaches.
• Gradual typing offers a spectrum from static to dynamic checks,
trading soundness for flexibility and interoperability.
• Refinement and liquid types push automated verification deeper, at the
cost of heavier solver involvement.
• Future work lies in integrating effects, resources, and dependently
typed abstractions in a gradual, user-friendly, and performant
framework—bridging the gap between research proof systems and everyday
software engineering.
- –