Strange Loop

A Little Taste of Dependent Types

Dependent types let us use the same programming language for compile-time and run-time code, and are inching their way towards the mainstream from research languages like Coq, Agda and Idris. Dependent types are useful for programming, but they also unite programming and mathematical proofs, allowing us to use the tools and techniques we know from programming to do math.

The essential beauty of dependent types can sometimes be hard to find under layers of powerful automatic tools. The Little Typer is an upcoming book on dependent types in the tradition of the The Little Schemer that features a tiny dependently typed language called Pie. We will demonstrate a proof in Pie that is also a program.

Come get a taste of Pie, and see for yourself where dependent types can take us.

David Christiansen

Galois, Inc.

David Christiansen is a researcher and engineer at Galois, Inc. He recently completed his PhD at the IT University of Copenhagen, working on metaprogramming and domain-specific languages in the dependently typed language Idris. Together with Dan Friedman, he is a co-author of The Little Typer, an upcoming book on dependent types in the tradition of The Little Schemer. David's main research goal is to make programming better by finding ways for programmers to express their goals and to then get help from the computer when achieving them.