Implementing Type-Level Literals in GHC[edit]

Iavor Diatchki

Type-level literals, such as natural numbers and string symbols, are useful for implementing safer Haskell libraries. For example, natural numbers in the types may be used to keep track of the sizes of various data structures (e.g., arrays or bit-vectors), while string symbols can be used as an infinite source of labels (e.g., to refer to statically known resources). In this talk, I will present some of the details of the implementation of type-level literals in GHC. In particular, I will discuss the overall design, the supporting libraries for programming with type-level literals, and demonstrate some techniques for writing programs with these libraries. Finally, I will give an update of the current state of the constraint solver, which adds support for type-level computation involving numbers.