Dependently typed programming with singletons

Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas are in-spired by dependently typed programs, the code looks significantly different. As a result, GHC implementors have responded with ex-tensions to Haskell’s type system, such as GADTs, type families, and datatype promotion. However, there remains a significant dif-ference between programming in Haskell and in full-spectrum de-pendently typed languages. Haskell enforces a phase separation be-tween runtime values and compile-time types. Therefore, singleton types are necessary to express the dependency between values and types. These singleton types introduce overhead and redundancy for the programmer. This paper presents the singletons library, which generates the boilerplate code necessary for dependently typed programming using GHC. To compare with full-spectrum languages, we present an extended example based on an Agda interface for safe database access. The paper concludes with a detailed discussion on the current capabilities of GHC for dependently typed programming and suggestions for future extensions to better support this style of programming