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