## 3 - Simply Typed Lambda Calculus

2019-10-18 10:00 CST
2019-11-01 12:00 CST
CC BY-NC 4.0

Adding types to $\lambda$-calculus:

• Classify functions using argument and result types
• Type-check function bodies, which have free variables

Simply-typed $\lambda$-calculus (STLC):

Suppose T is base types (int, bool, etc.),

$$\text{(Types) } \tau, \sigma ::= \text{T} \ \vert \ \tau \rightarrow \sigma$$

$\rightarrow$ is right-associative.

## Typing Judgement

Judgement: A statement $J$ about certain formal properties

• Has a derivation (proof): $\vdash J$
• Has a meaning (judgement semantics): $\vDash J$

$\Gamma \vdash M:\tau$ ($M$ is of type $\tau$ in context $\Gamma$)

• Typing context (a set of typing assumptions)
• $\Gamma ::= \cdot \ \vert \ \Gamma, x:\tau$
• Includes types of all the free variables in $M$
• Empty context $\cdot$ is for closed terms
• Under $\Gamma$, $M$ is a well-typed term of type $\tau$.

## Typing Rules

• var: $${ \over \Gamma, x:\tau \vdash x:\tau}$$
• app: $${\Gamma \vdash M:\sigma\rightarrow\tau \ \ \ \ \ \ \Gamma \vdash N:\sigma \over \Gamma \vdash MN:\tau}$$
• abs: $${\Gamma, x:\sigma \vdash M:\tau \over \Gamma \vdash (\lambda x:\sigma . M):\sigma\rightarrow\tau}$$

## Soundness and Completeness

• A sound type system never accepts a program that can go wrong
• No false negatives
• The langauge is type-safe
• A complete type system never rejects a program that cannot go wrong
• No false positives
• However, for any Turing-complete PL, the set of programs that may go wrong is undecidable
• Type system cannot be sound and complete
• Choose soundness, try to reduce false positives in practice

### Soundness

Theorem (Type Safety):

If $\cdot \vdash M:\tau$ and $M \rightarrow^* M'$, then $\cdot \vdash M':\tau$, and either $M' \in \text{Values}$ or $\exists M'', M' \rightarrow M''$

(the reduction of a well-typed term either diverges, or terminates in a value of the expected type)

• Preservation (subject reduction): well-typed terms reduce only to well-typed terms of the same type
• If $\cdot \vdash M:\tau$ and $M \rightarrow M'$, then $\cdot \vdash M':\tau$
• Progress: a well-typed term is either a value or can be reduced
• If $\cdot \vdash M:\tau$, then either $M' \in \text{Values}$ or $\exists M'', M' \rightarrow M''$

### Not Complete

The type system may reject terms that do not go wrong.

E.g. $(\lambda x.(x(\lambda y.y)) (x \ 3)) (\lambda z.z)$

• Cannot find $\sigma, \tau$ that $x:\sigma \vdash (x (\lambda y.y))(x \ 3) : \tau$ because we have to pick one type for $x$.
• But the term equals to 3.

### Strong Normalization Theorem

Well-typed terms in STLC always terminate.

### Product Type

Structures in C $\Leftrightarrow$ Products

• (Types) $\tau, \sigma ::= \dots \ \vert \ \sigma \times \tau$
• (Terms) $M, N ::= \dots \ \vert \ < M , N > \ \vert \ \text{proj1 } M \ \vert \ \text{proj2 } M$

Typing rules:

• pair $${\Gamma \vdash M:\sigma \ \ \ \ \Gamma \vdash N:\tau \over \Gamma \vdash < M , N >:\sigma\times\tau}$$
• proj1 $${\Gamma \vdash M:\sigma\times\tau \over \Gamma \vdash \text{proj1 }M:\sigma}$$
• proj2 $${\Gamma \vdash M:\sigma\times\tau \over \Gamma \vdash \text{proj2 }M:\tau}$$

### Sum Type

Unions in C, Subclasses in Java $\Leftrightarrow$ Sums

• (Types) $\tau, \sigma ::= \dots \ \vert \ \sigma + \tau$
• (Terms) $M, N ::= \dots \ \vert \ \text{left } M \ \vert \ \text{right } M \ \vert \ \text{case } M \text{ do } M1 \ M2$

case ... do ...: if $M$ is of type $\sigma$ then $M1$, otherwise $M2$

### Products vs. Sums

• Logical duals
• To make a $\sigma \times \tau$, we need a $\sigma$ and a $\tau$
• To make a $\sigma + \tau$, we need a $\sigma$ or a $\tau$
• Given a $\sigma \times \tau$, we can get a $\sigma$ or a $\tau$ or both (our choice)
• Given a $\sigma + \tau$, we must be prepared for either a $\sigma$ or a $\tau$ (the value’s choice)

## Recursion

Strong normalization theorem: well-typed terms in STLC always terminate.

However, recursion is not allowed by the typing rules (there is no types for fixed-point combinators).

Therefore we need an explicit construct for recursion: define a new type $\textbf{fix } M$ in terms.

Reduction rules for fix:

$${ \over \textbf{fix } \lambda x.\ M \rightarrow M[\textbf{fix } \lambda x.\ M / x]}$$

$${M \rightarrow M' \over \textbf{fix } M \rightarrow \textbf{fix } M'}$$

Typing rule for fix:

$${\Gamma \vdash M : \tau \rightarrow \tau \over \Gamma \vdash \textbf{fix } M : \tau}\ (\text{fix})$$

## Curry-Howard Isomorphism

What we did:

• Programming language
• A type system to rule out “bad” programs

What logicians do:

• Define logic propositions
• Defina a proof system to prove “good” propositions

Isomorphism (Slogan):

• Propositions are Types
• Propositions: $\text{boolean} \vert p \Rightarrow q \vert p \wedge q \vert p \vee q$
• Types: $\text{T} \vert \sigma \rightarrow \tau \vert \sigma \times \tau \vert \sigma + \tau$
• Proofs are Programs

Different types:

• Nonempty types: closed terms of that type
• Empty types: non closed terms of that type
• How do we know whether a type is empty?
• Replace $\rightarrow$ with $\Rightarrow$, $\times$ with $\wedge$, $+$ with $\vee$
• Nonempty types can be proved in propositional logic
• Empty types cannot be proved in propositional logic

Curry-Howard Isomorphism:

• Given a well-typed closed term, take the typing derivation, erase the terms, and have a propositional-logic proof
• Gien a propositional-logic proof, there exists a closed term with that type
• A term that type-checks is a proof
• Constructive propositional logic and STLC with pairs and sums are the same thing

Classical v.s. Constructive

Law of the ecluded middle: $${\over \Gamma \vdash p \vee (p \Rightarrow q)}$$

STLC does not support it: no closed term has type $\rho + (\rho \rightarrow \sigma)$.

Logics without this rule are called “constructive” or “intuitionistic”. Formulas are only considered “true” when we have direct evidence.

Transform to constructive logic: if any number is either rational or irrational, then there exists two irrational numbers …

A valid proof must terminate, however the reduction of $\textbf{fix}$ does not terminate. Thus including $\textbf{fix}$ would make the logic inconsistent.