Dependent Types

Tikhon Jelvis (tikhon@jelv.is)

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

$$ \newcommand{\ty}[1]{\mathbf{#1}} $$ $$ \newcommand{\N}[0]{\mathbb{N}} $$ $$ \newcommand{\kd}[0]{\ty{\star}} $$

1 Untyped λ-calculus

  • terms: functions (λ), variables, application

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

  • evaluation via substitution:

$$ (\lambda x. e)s \Rightarrow [s/x]e $$

2 Simply typed λ-calculus

  • extend untyped λ-calculus with “simple” types
  • simple: atomic “base” types + functions
    • base: \(\ty{unit}\), \(\ty{int}, \ldots\)
    • function: \(\ty{unit} \to \ty{unit}, \ldots\)
  • not Turing-complete any more
    • safety at the expense of expressiveness

3 Simply typed λ-calculus

  • new type-level syntax

$$\begin{align} \tau ::&= \ty{unit} & \text{unit type}\\ &|\quad \tau_1 \to \tau_2 & \text{function types}\\ \newline e ::&= () & \text{unit value}\\ &|\quad x & \text{variable}\\ &|\quad \lambda x:\tau. e & \text{abstraction}\\ &|\quad e_1 e_2 & \text{application} \end{align}$$

  • evaluation is unchanged

4 System F

  • parametric polymorphism
  • allow “families” of simply typed terms
    • polymorphic \(id\) is a family of \(id_{\ty{unit}}, id_{\ty{int}}, id_{\ty{int \to int}}, \ldots\)
  • a “family” is a function from types to values

5 System F

$$\begin{align} \tau ::&= \ty{unit} & \text{unit type}\\ &|\quad \alpha & \text{type variable}\\ &|\quad \tau_1 \to \tau_2 & \text{function types}\\ &|\quad \forall\alpha.\tau & \text{type quantification}\\ \newline e ::&= () & \text{unit value}\\ &|\quad x & \text{variable}\\ &|\quad \lambda x:\tau. e & \text{abstraction}\\ &|\quad e_1 e_2 & \text{application}\\ &|\quad \Lambda\alpha. e & \text{type abstraction}\\ &|\quad e_1[\tau] & \text{type application} \end{align}$$

6 Type abstractions

  • type functions: \(\Lambda\alpha. \tau\)
  • qualified types: \(\forall\alpha. \tau\)
  • type application: \(e_1[\tau]\)
  • example: $$ \begin{align} &id : \forall\alpha. \alpha \to \alpha \\ &id = \Lambda\alpha.\lambda (x:\alpha). x \\ \end{align}$$

7 Type abstractions

  • hey, these are like normal λs, but simpler
  • functions: \(\lambda (x : \tau). e\)
  • function types: \(\tau_1 \to \tau_2\)
  • function application: \(e_1\ e_2\)

8 Unifying types and terms

  • let's combine these two similar constructs
  • everything is a term
    • values can appear in types
    • no more clean type/value separation

9 Why?

  • System F: repetition over different types
    • \(id_{\ty{unit}}, id_{\ty{int}}, id_{\ty{int \to int}}, \ldots\)
  • consider other repetitive patterns:
    • \(\ty{int}, \ty{int \times int}, \ty{int \times int \times int}, \ldots\)
    • \(\ty{vector}\ 1, \ty{vector}\ 2, \ty{vector}\ 3, \ldots\)
  • we would love to write $$ dot : \ty{vector}\ n \times \ty{vector}\ n \to int $$

10 Dependent types

  • no type syntax: \(e\) and \(\tau\) are expressions

$$\begin{align} e, \tau ::&= () & \text{unit value}\\ &|\quad \ty{unit} & \text{unit type}\\ &|\quad \ty{\star} & \text{type of types}\\ &|\quad x & \text{variable}\\ &|\quad \forall (x:\tau). \tau' & \text{dependent function}\\ &|\quad e_1\ e_2 & \text{application}\\ &|\quad \lambda (x:\tau). e & \text{abstraction}\\ \end{align} $$

  • \(\forall (x:\tau). \tau'\) replaces function arrows (\(\to\))

11 Typing rules: types of types

  • What type does \(\ty{\star}\) have?
    • simple (but dubious) answer: \(\ty{\star} : \ty{\star}\)
    • more interesting: infinite hierarchy \(\ty{\star_1} : \ty{\star_2} : \ty{\star_3} : \ldots\)
  • let's go with simplicity: $$ \frac{}{\Gamma \vdash \ty{\star} : \ty{\star}} $$

12 Typing rules: dependent abstractions

  • dependent abstractions are terms too:

$$ \frac{\Gamma \vdash \tau : \ty{\star}\quad \Gamma, x : \tau \vdash \tau' : \ty{\star}}{\Gamma \vdash (\forall (x : \tau). \tau') : \ty{\star}} $$

  • key idea: \(\tau'\) can depend on \(x\)
  • \(\forall (x : \tau). \tau'\) is like a function type \(\tau \to \tau'\) except also parametrized by a value \(x\)
    • alternative syntax: \((x : \tau) \to \tau'\)

13 Typing rules: application

  • remember: the new function type is a \(\forall\):

$$ \frac{\Gamma \vdash e_1 : \forall (x : \tau). \tau' \quad \Gamma \vdash e_2 : \tau}{\Gamma \vdash e_1\ e_2 : [e_2/x]\tau'} $$

  • substitution happening at the type level
    • basically like enabling the type system with evaluation

14 Typing rules: type equivalence

  • since types are terms, we need to evaluate them to check for equivalence
  • read \(e_1 \Downarrow e_2\) as “\(e_1\) evaluates to \(e_2\) ”

$$ \frac{\Gamma \vdash e : \tau_1 \quad \tau_1 \Downarrow \tau \quad \tau_2 \Downarrow \tau}{\Gamma \vdash e : \tau_2} $$

  • consider: \(\ty{vector}\ 5\) vs \(\ty{vector}\ (2 + 3)\) vs \(\ty{vector}\ (3 + 2)\)
  • again: evaluation in type checking

15 Typing rules: abstractions

  • pretty straightforward: \(\to\) just becomes \(\forall\):

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

  • note: \(x\) can occur in body and type

16 Example: id

  • from System F: $$ \begin{align} &id : \forall\alpha. \alpha \to \alpha \\ &id = \Lambda\alpha.\lambda (x:\alpha). x \\ \end{align}$$
  • with dependent types: $$ \begin{align} &id : \forall(\alpha : \ty{\star}). (\forall (x : \alpha). \alpha) \\ &id = \lambda (\alpha : \ty{\star}). (\lambda (x : \alpha). x) \\ \end{align}$$
  • the System F \(\Lambda\) has become a normal \(\lambda\) !

17 Nicer notation

  • often, we just want normal functions
    • ignore argument \(x\)
  • special syntax: \(\to\)
  • consider \(id\): \(\forall (\alpha : \kd). \alpha \to \alpha\)
  • no extra name (\(x\)) introduced

18 Example: vectors

  • assume built-in numbers: \(\N : \ty{\star}\) and \(n : \N\)
  • vectors indexed by length: $$\forall (\alpha : \ty{\star}). \forall (n : \N). \ty{vec}\ \alpha\ n$$
  • constructors:

$$ \begin{align} &Nil : \forall (\alpha : \kd). \ty{vec}\ \alpha\ 0\\ &Cons : \forall (\alpha : \kd). \forall (n : \N). \alpha \to\\ & \ty{vec}\ \alpha\ n \to \ty{vec}\ \alpha\ (n + 1) \\ \end{align} $$

19 Example: zero vector

  • we can have sized vectors in Haskell
    • numbers at the type level—redundant
  • however, Haskell can't do this:

$$ zero : \forall(n : \N). \ty{vec}\ \ty{int}\ n $$

  • creates a vector of length \(n\), full of \(0\) s
  • argument \(n\) is part of result type!