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

Implementation and Design Issues

• Implementation of GHC.TypeNats
• Alternative Design For Singletons

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

External links

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