A taste of dependent types

Keegan McAllister

May 15, 2015

Navigate with ← and → keys, or view all slides.

Available at kmcallister.github.io

Dependent types

Types are first-class values

Argument type can depend on value of prior argument

fn foo(T: type, n: usize, v: &Vec(T, n)) {
    ...
}

Why might we want this in Rust?

Simplify the compile-time language
Prove correctness of programs and APIs
Eliminate overhead of run-time checks
Clean up the syntax — no more f::<T>(x)

Refinement types

Known in industry as design by contract.

Fits perfectly in Rust syntax!

fn index(T: type, x: &[T], i: usize) -> &T
    where i < x.len()
{
    ...
}

Data invariants

This binary tree is always in search order:

fn range(lo: isize, hi: isize) -> type {
    those x: isize where lo <= x && x < hi
}

enum Tree(lo: isize, hi: isize) {
    Empty,
    Node {
        val: range(lo, hi),
        left: Tree(lo, val),
        right: Tree(val, hi),
    },
}

Subtyping based on logical implication is undecidable.

Compiler asks an “off-the-shelf” theorem prover.

Answer is “yes”, “no”, or “maybe” (⇒ check at runtime).

Refinement extensions exist for C, ML, Haskell, C#, F#

miTLS (live demo) is a verified SSL/TLS stack.

They found a protocol bug too!

(Co-)inductive constructions

A different approach to dependent types.

Calculus of constructions + generalized algebraic data types

Programs are proofs (Curry-Howard correspondence)

Programs are correct by construction

Defining an inductive type

Each enum constructor specifies its type.

enum Nat {
    Zero: Nat,
    Succ(Nat): Nat,
}

enum Vec(T: type, len: Nat) {
    Nil:
        Vec(T, Nat::Zero),

    Cons(T, Vec(T, len)):
        Vec(T, Nat::Succ(len)),
}

Inductive data can refine, too

enum Equal(T: type, a: T, b: T) {
    Refl: Equal(T, a, a),
}

struct Refine(T: type, p: T -> bool) {
    value: T,
    proof: Equal(bool, true, p(value)),
}

fn range(lo: isize, hi: isize) -> type {
    Refine(isize, |x| lo <= x && x < hi)
}

enum Tree ... // as before