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 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 as well, and allowing us to run our proofs as programs.
The essential beauty of dependent types can sometimes be hard to find under layers of powerful automatic tools. Dan Friedman and I have been working on a presentation of the fundamental ideas in The Little Typer, an upcoming book in the tradition of The Little Schemer. As part of the effort, we have created Pie. Pie is a little dependently typed language, small enough to understand completely but big enough to write a variety of proofs and programs.
Come get a taste of Pie, and see for yourself where dependent types can take us.
David Christiansen works at the border between type theory and type practice. Together with Dan Friedman, he is a co-author of the upcoming book The Little Typer, a friendly introduction to the essential ideas behind dependent types. He has done work on Idris, especially its interactive environment and metaprogramming facilities, as well as work on integrating Racket’s macro system with a dependent type theory. Now, he is a researcher/engineer at Galois, Inc.