Tikhon Jelvis (tikhon@jelv.is)

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}{\mathbf{#1}}$$ $$\newcommand{\ite}{\text{if }#1\text{ then }#2\text{ else }#3}$$ $$\newcommand{\case}{\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

• 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

• 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