Polymorphism

Tikhon Jelvis (tikhon@jelv.is)

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

$$ \newcommand{\ty}[1]{\mathbf{#1}} $$

1 Untyped λ-Calculus

  • model computation with functions
  • simple structure:

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

2 λ-Calculus Evaluation

  • key idea: application by substitution

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

  • \([s/x]e\) = “replace \(x\) with \(s\) in \(e\) ”
  • handy mnemonic (thanks Sergei): multiplying by \(\frac{s}{x}\) and canceling
  • remember to worry about “capturing”

3 Simple Types

  • extend λ-calculus with types
  • base types
    • \(\ty{unit}\), \(\ty{int}\)… etc
  • function types
    • \(\ty{int} \to \ty{int}\)
    • \((\ty{unit} \to \ty{unit}) \to \ty{int} \to \ty{int}\)

4 Syntax: Terms and Types

$$\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}$$

5 Typing Rules

  • functions:

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

  • application:

$$ \frac{\Gamma \vdash e_1 : \tau \to \tau' \quad \Gamma \vdash e_2 : \tau}{\Gamma \vdash e_1 e_2 : \tau'} $$

6 Problem: Repetition

  • every type has an identity function: $$\lambda x : \tau. x$$
  • different for every possible \(\tau\)

$$id_{\ty{unit}}, id_{\ty{int}}, id_{\ty{int \to int}} \ldots$$

  • a single term can have multiple incompatible types

7 Solution: System F

  • add polymorphism to our types
    • types parameterized by other types
  • what is a “parameterized term”x?
    • λ abstraction (function)
  • so: function for types
  • \(id\) would take a type \(\tau\) and give you \(id_\tau\)

8 New Syntax

$$\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}$$

9 Type Variables

  • behave mostly like value-level variables
  • type variables can be free or bound
    • free variables are not defined inside expression
  • substitute types for type variables:
    • \([\sigma/\alpha]\tau\) means “replace α with σ in type τ”

10 Evaluation

  • simply typed λ-calculus—just like untyped:

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

  • one more rule, for type abstractions:

$$ (\Lambda\alpha. e)[\tau] \Rightarrow [\tau/\alpha]e $$

  • type-level version of the first rule
  • reduction is still very simple

11 Typing Rules

  • \(\Gamma\) now covers both type and term variables
  • basic rules just like STLC
  • new rules:

$$ \frac{\Gamma, \alpha \vdash x : \tau}{\Gamma \vdash \Lambda\alpha. x : \forall\alpha. \tau} $$ $$ \frac{\Gamma \vdash x : \forall\alpha. \tau}{\Gamma \vdash x[\sigma] : ([\sigma/\alpha]\tau)} $$

  • compare to normal abstraction and application

12 Running Example: id

  • function: $$ \begin{align} &id : \forall\alpha. \alpha \to \alpha \\ &id = \Lambda\alpha.\lambda (x:\alpha). x \\ \end{align}$$
  • reduction: $$ \begin{align} & (\Lambda\alpha.\lambda (x:\alpha). x)[\ty{unit}] () \\ \Rightarrow & (\lambda (x:\ty{unit}). x) () \\ \Rightarrow & () \\ \end{align}$$

13 Another Example: app

  • Untyped term, impossible in STLC: $$\lambda f. \lambda x. f x$$
  • we can type function application:

$$ \begin{align} &app : \forall\alpha. \forall\beta. (\alpha \to \beta) \to \alpha \to \beta\\ &app = \Lambda\alpha. \Lambda\beta.\lambda (f : \alpha \to \beta). \lambda (x : \alpha). f x \end{align} $$

  • Haskell $, OCaml <|: really just \(id\) with restricted type

14 Interesting Example: self application

  • We cannot even express self-application in STLC

$$ \lambda f. f f $$

  • but we can with polymorphism:

$$ \begin{align} & self : (\forall\alpha. \alpha \to \alpha) \to (\forall \beta. \beta \to \beta) \\ & self = \lambda (f : \forall\alpha. \alpha \to \alpha). f[\forall\beta. \beta \to \beta] f \end{align} $$

  • however, still no infinite loops

15 Data Structures

  • consider untyped booeans:

$$ \begin{align} true &= \lambda x. \lambda y. x \\ false &= \lambda x. \lambda y. y \end{align} $$

  • typed version:

$$ \begin{align} true, false &: \forall \alpha. \alpha \to \alpha \to \alpha \\ true &= \Lambda\alpha. \lambda (x : \alpha). \lambda (y : \alpha). x \\ false &= \Lambda\alpha. \lambda (x : \alpha). \lambda (y : \alpha). y \end{align} $$

  • types prevent malformed “booleans”

16 Products

  • easy in untyped λ; added to STLC explicitly:

$$ \begin{align} \sigma \times \tau &: \forall\alpha. (\sigma \to \tau \to \alpha) \to \alpha \\ \langle s, t\rangle &= \Lambda\alpha.\lambda (f : \sigma \to \tau \to \alpha). f s t \\ \newline fst &: \sigma \times \tau \to \sigma \\ fst &= \lambda (p : \sigma \times \tau). p[\sigma](\lambda s : \sigma. \lambda t : \tau. s) \end{align} $$

  • we can do sum types similarly

17 Type Inference

  • this is a handy system
  • unfortunately, type inference is undecideable
  • we can make type inferrable with a simple restriction:
    • prenex form: all quantifiers at the front
    • types where all foralls are left of parentheses
  • Haskell, ML… etc do this

18 Hindley-Milner

  • important insight: most general type
  • every untyped term has a unique most general type

$$ \lambda x. x : \forall\alpha. \alpha \to \alpha $$

  • we can easily model this with logic programming
    • faster algorithms exist as well

19 Curry-Howard

  • System F maps to 2nd-order logic
    • quantifiers only over predicates
  • predicate logic with \(\forall\) but no “domains”
    • no external sets to quantify over
  • consider: \(\Lambda\) defines a function from types to values
    • but not vice-versa

20 Experimenting

  • Standard Haskell, ML… etc: prenex form
  • Haskell with RankNTypes: everything we've covered
    • along with recursion and recursive types
  • OCaml can also do the equivalent of RankNTypes but awkwardly