Type-level natural numbers
Natural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time (e.g., sub-range types in Pascal, array type in C, etc.). The feature is particularly useful when combined with polymorphism as illustrated by more recent programming languages (e.g., Cyclone, BlueSpec, Cryptol, Habit).
Existing features of Haskell's type system---such as polymorphism, kinds, and qualified types---make it particularly suitable for adding support for type level naturals in a natural way!
Indeed, there are quite a few Haskell libraries available on Hackage that implement support for type-level numbers in various forms. These libraries are being used by other packages and projects (e.g., the Kansas Lava project, and the type-safe bindings to the LLVM library).
Supporting natural number types directly in the compiler would help these projects, and others, by improving on the existing libraries in the following ways:
- a standard implementation,
- a better notation,
- better error messages,
- a more efficient implementation,
- more complete support for numeric operations.
I have started on an implementation of this feature, and my GHC branch is available in a darcs repository at the following URL:
http://code.galois.com/darcs/ghc-type-naturals/Trac metadata
| Trac field | Value |
|---|---|
| Version | |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |