Version 25 (modified by 9 years ago) (diff) | ,
---|
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
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
- XXX: Write the new rules
- Translation to FC
- Precedences for infix predicates such as ~ and <=
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