Adding Types

Tikhon Jelvis (tikhon@jelv.is)

Press → key to advance.
Zoom in/out: Ctrl or Command + +/-

1 Untyped Lambda Calculus

simple model of functions
few parts:

$$\begin{align} e ::&= x & \text{variable}\\ &|\quad \lambda x. e & \text{abstraction} \\ &|\quad e_1 e_2 & \text{application} \end{align}$$

2 Untyped Lambda Calculus

simple evaluation
just function application!

$$ \frac{(\lambda x. e) e'}{[e'/x]e} $$

replace $x$ with the argument in the body

3 The Song that Never Ends

Lambda calculus is Turing-complete (Church-Turing thesis)
infinite loops:

$$ (\lambda x. x x) (\lambda y. y y) \Rightarrow (\lambda y. y y) (\lambda y. y y)$$

good for programming, bad for logic

4 Preventing Self-Application

problem: self-application
- $xx$ leads to infinite loops
we need a rule to prevent self-application (and infinite loops in general)
- simple
- syntactic
- static
conservative by necessity

$$ \newcommand{\t}[1]{\mathbf{#1}} $$ $$ \newcommand{\ite}[3]{\text{if }#1\text{ then }#2\text{ else }#3} $$ $$ \newcommand{\case}[5]{\text{case }#1\text{ of }#2 \to #3 \quad|\ #4 \to #5} $$

5 Why?

helps lambda calculus as a logic
provides simple model of real type systems
helps design new types and type systems
usual advantages of static typing

6 Base Types

start with some "base" types (like axioms)
- ints, booleans… whatever
even just the $\t{unit}$ type is fine
base types have values:
- $()$ is of type $\t{unit}$
- $1$ is of type $\t{int}$
ultimately, the exact base types don't matter

7 Function Types

one type constructor: $\to$ (like axiom schema)
represents function types
$\t{unit} \to \t{unit}$
$\t{int} \to \t{unit} \to \t{int}$
values are functions

8 Assigning Types

we need some way to give a type to an expression
only depends on the static syntax
typing judgement: $x : \tau$

9 Context

depends on what's in scope (typing context): $$ \Gamma \vdash x : \tau $$
things in scope: "context", $\Gamma$
set of typing judgements for free variables:$$\Gamma = \{x : \tau, y : \tau \to \tau, ... \}$$

10 New Syntax

$$\begin{align} \tau ::&= \t{unit} & \text{unit type}\\ &|\quad \t{int} & \text{int type}\\ &|\quad \tau_1 \to \tau_2 & \text{function types} \end{align}$$

$$\begin{align} e ::&= () & \text{unit value}\\ &|\quad n & \text{integer}\\ &|\quad e_1 + e_2 & \text{arithmetic}\\ &|\quad x & \text{variable}\\ &|\quad \lambda x:\tau. e & \text{abstraction}\\ &|\quad e_1 e_2 & \text{application} \end{align}$$

11 Typing Rules

we can assign types following a few "typing rules"
idea: if we see expression "x", we know "y"
just like implication in logic $$ \frac{\text{condition}}{\text{result}} $$
remember the context matters: $\Gamma$

12 Base rules

note: no prerequisites!

$$ \frac{}{\Gamma \vdash n : \t{int}} $$ $$ \frac{}{\Gamma \vdash () : \t{unit}} $$

base cases for recursion

13 Main Rules

contexts:

$$ \frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau} $$

function bodies:

$$ \frac{\Gamma, x : \tau \vdash e : \tau'}{\Gamma \vdash (\lambda x:\tau. e) : \tau \to \tau'} $$

14 Main Rules

application:

$$ \frac{\Gamma \vdash e_1 : \tau \to \tau' \quad \Gamma \vdash e_2 : \tau}{\Gamma \vdash e_1 e_2 : \tau'} $$

recursive cases in the type system
think of a function over syntactic terms
- similar to evaluation!

15 Domain-Specific Rules

we add rules for our "primitive" operations

$$ \frac{\Gamma \vdash e_1 : \t{int} \quad \Gamma \vdash e_2 : \t{int}}{\Gamma \vdash e_1 + e_2 : \t{int}} $$

imagine other base types like booleans

$$\frac{\Gamma \vdash c : \t{bool} \quad \Gamma \vdash e_1 : \tau \quad \Gamma \vdash e_2 : \tau}{\Gamma \vdash \ite{c}{e_1}{e_2} : \tau} $$

easy to extend

16 No Polymorphsim

we do not have any notion of polymorphism
function arguments have to be annotated
untyped: $\lambda x. x$
typed:
- $\lambda x:unit. x$
- $\lambda x:int. x$
- $\lambda x:int \to unit \to int. x$

17 Numbers

remember numbers as repeated application
untyped:
- 0: $\lambda f. \lambda x. x$
- 1: $\lambda f. \lambda x. f x$
- 2: $\lambda f. \lambda x. f (f x)$
- 3: $\lambda f. \lambda x. f (f (f x))$

18 Typed Numbers

we can add types:
- 0: $\lambda f : \t{unit} \to \t{unit}. \lambda x : \t{unit}. x$
- 1: $\lambda f : \t{unit} \to \t{unit}. \lambda x : \t{unit}. f x$
- 2: $\lambda f : \t{unit} \to \t{unit}. \lambda x : \t{unit}. f (f x)$
- 3: $\lambda f : \t{unit} \to \t{unit}. \lambda x : \t{unit}. f (f (f x))$
numbers: $(\t{unit} \to \t{unit}) \to \t{unit} \to \t{unit}$

19 Pairs

remember pair encoding:
- cons: $\lambda x. \lambda y. \lambda f. f x y$
- first: $\lambda x. \lambda y. x$
- second: $\lambda x. \lambda y. y$
lets us build up data types, like lisp

20 Typed Pairs

cons: $$ \lambda x : \tau. \lambda y : \tau . \lambda f : \tau \to \tau \to \tau. f x y$$
but we want pairs of different types!
we should add pairs ("product types") to our system

21 Product Types

new type syntax: $\tau_1 \times \tau_2$
like Haskell's (a, b) or OCaml's a * b
constructor:

$$ \frac{\Gamma \vdash e_1 : \tau_1 \quad \Gamma \vdash e_2 : \tau_2}{\Gamma \vdash (e_1, e_2) : \tau_1 \times \tau_2}$$

22 Product Types

accessors ($\text{first}$ and $\text{second}$):

$$ \frac{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash \text{first } e : \tau_1} $$ $$ \frac{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash \text{second } e : \tau_2} $$

23 Sum Types

sum types: disjoint/tagged unions, variants
like Haskell's Either
new type syntax: $\tau_1 + \tau_2$
construction:

$$ \frac{\Gamma \vdash e : \tau_1}{\Gamma \vdash \text{left } e : \tau_1 + \tau_2} $$ $$ \frac{\Gamma \vdash e : \tau_2}{\Gamma \vdash \text{right } e : \tau_1 + \tau_2} $$

24 Sum Types

matching

$$ \frac{\Gamma\ \vdash\ e : \tau_1 + \tau_2 \atop \Gamma,\ x : \tau_1 \ \vdash\ e_1 : \tau' \quad \Gamma,\ y : \tau_2 \ \vdash\ e_2 : \tau'}{\Gamma \vdash (\case{e}{x}{e_1}{y}{e_2}) : \tau'}$$

25 Algebraic Data Types

this basically gives us algebraic data types
now we just need recursive types and polymorphism