Depending on types

Abstract

Is Haskell a dependently typed programming language? Should it be? GHC's many type-system features, such as Generalized Algebraic Datatypes (GADTs), datatype promotion, multiparameter type classes, and type families, give programmers the ability to encode domain-specific invariants in their types. Clever Haskell programmers have used these features to enhance the reasoning capabilities of static type checking. But really, how far have we come? Could we do more?