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
• Natural Numbers: From Values to Types
• Type-Level Operations

Notes on Design

• Alternative Design For Singletons
• Avoiding Partial Type Functions
• Naturals or Integers?

Notes on the Implementation

• Implementation of GHC.TypeNats
• Axioms for Natural Number Operators
• GHC Interaction Rules (Notational Conventions)
  • Top-Level Interactions
  • Simple Inert Interactions
  • Solving (<=) Predicates

External links

• The implementation resides in several repositories:
  • (GIT) Changes to GHC are on branch type-nats in:  git://code.galois.com/type-naturals/ghc.git
  • (DARCS) Changes to the base library are at  http://code.galois.com/darcs/type-naturals/09-Jan-2011/base/
  • (DARCS) Changes to the template-haskell library are at  http://code.galois.com/darcs/type-naturals/09-Jan-2011/template-haskell/

• More advanced example:  https://github.com/yav/memory-arrays/tree/master