Type Level Naturals

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

User's Guide

• Type-Level Naturals Basics
• Type-Level Computation
• Typed examinations of TNat (inductive definitions)

Notes on Design

• Alternative Design For Singletons
• Avoiding Partial Type Functions

Notes on the Implementation

• Implementation of GHC.TypeNats
•  Axioms for type-level type operators

External links

• The implementation resides on branch 'type-nats' of the GHC repo. The following GHC-related related repos also have a type-nats branch:
  • libraries/base
  • libraries/template-haskell
  • utils/haddock

XXX: Cleanup

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