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?

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) {
    Node {
        val: range(lo, hi),
        left: Tree(lo, val),
        right: Tree(val, hi),

Implementing refinements

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) {
        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

Using inductive data

Hand-written proofs based on pattern matching.

Help from editor integration or automated “proof tactics”.


Coq supports compiling to Haskell, OCaml, Scheme...

How about Rust? Work is underway.

Dependent types for Rust?

Sounds like a fantasy...

So did “concurrent memory safety for C++”.

What will Rust and its offspring look like in another decade?

What to read next

Pierce et al. Software Foundations.
Free online w/ machine-guided exercises!

Norell & Chapman. “Dependently Typed Programming in Agda

The Idris documentation.

Pierce. (2002). Types and Programming Languages. MIT Press.

Other recommended reading

Gronski, J., Knowles, K., Tomb, A., Freund, S. N., & Flanagan, C. (2006). Sage: Hybrid checking for flexible specifications. Scheme and Functional Programming Workshop (pp. 93-104).

Harper, R. (2012). Practical Foundations for Programming Languages (draft online). Cambridge University Press.

Löh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Fundamenta informaticae, 102(2), pp. 177-207.

Ou, X., Tan, G., Mandelbaum, Y., & Walker, D. (2004). Dynamic typing with dependent types. Exploring New Frontiers of Theoretical Informatics (pp. 437-450). Springer US.

Pierce, B. (Ed.) (2005). Advanced Topics in Types and Programming Languages. MIT Press.

Rondon, P. M., Kawaguci, M., & Jhala, R. (2008). Liquid types. ACM SIGPLAN Notices 43(6), pp. 159-169.

Wadler, P., & Findler, R. B. (2009). Well-typed programs can’t be blamed. Programming Languages and Systems (pp. 1-16). Springer Berlin Heidelberg.