#4385: Type-level natural numbers
---------------------------------+------------------------------------------
Reporter: diatchki | Owner: diatchki
Type: feature request | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: | Keywords:
Testcase: | Blockedby:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
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/
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
