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

Prerequisites:

 * 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/

 

.