Keegan McAllister

May 15, 2015

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

Available at `kmcallister.github.io`

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

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() { ... }

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!

A different approach to dependent types.

*Calculus of constructions* + *generalized algebraic data types*

Programs *are proofs* (Curry-Howard correspondence)

Programs are correct *by construction*

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)), }

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

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.

Sounds like a fantasy...

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

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

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.

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.