David Christiansen

A Little Taste of Types
Workshop: Implementing Dependent Types

Postdoc at IU Bloomington

A Little Taste of 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. Unfortunately, the essential beauty of dependent types can sometimes be hard to find under layers of powerful automatic tools.

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.

Talk objectives:

 * Convey the core ideas of propositions as types, proofs as programs
 * Show the off the wonder and magic of dependent types in Pie

Target audience:

 * Anyone who is comfortable with parentheses and recursion


Workshop: Implementing Dependent Types

Dependent types are showing up in more and more mainstream languages, but they can still seem like magic. In this workshop, we'll walk through one of the primary techniques for implementing a type checker for dependent types, called normalization by evaluation. We'll be implementing a little dependently typed language called Pie developed by Dan Friedman and myself.

The implementation is written entirely in a very small subset of Scheme, and I'll assume no knowledge beyond that gained by reading The Little Schemer.

Workshop goals:

 * Introduce the ideas behind normalization by evaluation and
   bidirectional type checking

 * Write a type checker for a little dependently typed language


 * Basic familiarity with and interest in dependent types, equivalent
   to having worked through the Idris tutorial [1]

 * Know enough Racket or Scheme to write an interpreter for a small
   Lisp-like language

 * Have a recent version of Racket installed on your laptop

[1]: http://docs.idris-lang.org/en/latest/tutorial/



About David

David works at the border between type theory and type practice. He has done work on Idris, especially its interactive environment and metaprogramming facilities, and is currently working on integrating proofs and macros in Racket.

Github: david-christiansen

Twitter: @d_christiansen

Back to conference page