## Adding Types

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.

## Adding Stuff

### 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

Recall: Fixpoint combinator in untyped $\lambda$-calculus

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.

## Loading Comments By Disqus