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
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'sa * 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