|Version 27 (modified by diatchki, 15 months ago)|
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).
Notes on Design
- Alternative Design For Singletons
- Avoiding Partial Type Functions
- Naturals or Integers?
- Inductive definitions
Notes on the Implementation
- Implementation of GHC.TypeNats
- Axioms for Natural Number Operators
- GHC Interaction Rules (Notational Conventions)
- Translation to FC
- Precedences for infix predicates such as ~ and <=
- The implementation resides on branch 'type-nats' of the GHC repo. The following GHC-related related repos also have a type-nats branch:
- More advanced example: https://github.com/yav/memory-arrays/tree/master