  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.
