Dependent Types
Tikhon Jelvis (tikhon@jelv.is)
Press → key to advance.
Zoom in/out: Ctrl or Command + +/-
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!