Dependent Types in Haskell: Theory and Practice

TL;DR

This paper introduces Dependent Haskell, an extension to GHC that enables full dependent types, along with an implementation, practical examples, and a type inference algorithm, bridging the gap between Haskell and dependently typed programming.

Contribution

It presents the design and partial implementation of Dependent Haskell, a backward-compatible extension supporting full dependent types in GHC, with a novel intermediate language and inference algorithm.

Findings

Implemented features are available in GHC 8.0.

Demonstrated practical examples of dependently typed Haskell code.

Developed Pico, a dependently typed lambda-calculus for compilation.

Abstract

Haskell, as implemented in the Glasgow Haskell Compiler (GHC), has been adding new type-level programming features for some time. Many of these features---chiefly: generalized algebraic datatypes (GADTs), type families, kind polymorphism, and promoted datatypes---have brought Haskell to the doorstep of dependent types. Many dependently typed programs can even currently be encoded, but often the constructions are painful. In this dissertation, I describe Dependent Haskell, which supports full dependent types via a backward-compatible extension to today's Haskell. An important contribution of this work is an implementation, in GHC, of a portion of Dependent Haskell, with the rest to follow. The features I have implemented are already released, in GHC 8.0. This dissertation contains several practical examples of Dependent Haskell code, a full description of the differences between Dependent Haskell and today's Haskell, a novel type-safe dependently typed lambda-calculus (called Pico) suitable for use as an intermediate language for compiling Dependent Haskell, and a type inference and elaboration algorithm, Bake, that translates Dependent Haskell to type-correct Pico.