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).

• Type-Level Naturals Basics
• Simple Examples of Using GHC.TypeNats
• Implementation of GHC.TypeNats
• Design Notes about Nat vs. TypeNat
• Axioms for Natural Number Operators
• GHC Interaction Rules
  • Top-Level Interactions
  • Simple Inert Interactions
  • [wiki:TypeNats/LEQ Solving <= Predicates

External links:

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