Type Level Literals

This page collects information on how to work with type-level literals, as implemented in the Haskell compiler GHC (ticket #4385).

User's Guide

• Type-Level Literal Basics
• Type-Level Computation
• Typed examinations of Sing values
• Matching on Type-Level Naturals (i.e., working with classes and type-families)

Notes on Design

• Details about the implementation of singleton families.
• Alternative Design For Singletons
• Avoiding Partial Type Functions
• Singletons and Existentials

Notes on the Implementation

• Implementation of GHC.TypeLits
• The solver for type-level naturals

Source Code

•  type-nats branch of GHC
•  type-nats branch of the base library
•  type nats branch of template-haskell
• Also, there is a type-nats branch for 'haddock'.

XXX: Cleanup

• Natural Numbers: From Values to Types
• More advanced example:  https://github.com/yav/memory-arrays/tree/master
• Examples
•  Axioms for type-level type operators