[Haskell-cafe] Announce type-level-natural-number-1.0: Simple, Haskell 2010-compatible type level natural numbers

[Alexey Khudyakov]

On Fri, 30 Jul 2010 13:28:19 -0700
Gregory Crosswhite <gcross at phys.washington.edu> wrote:
>  Hey everyone,
> 
> I am pleased to announce the release of the "type-level-natural-number"
> package, which implements natural numbers at the type level.  Although
> there are many packages on Hackage that implement type level natural
> numbers, this package is distinguished by its simplicity: it does not
> offer any operations other than predecessor, successor, and conversion
> to Int, and so the only Haskell extension it needs is EmptyDataDecls. 
> Thus, this package is compatible with Haskell 2010.
> 
> The envisioned use case is for annotating types with natural numbers, so
> that extra functionality such as addition and subtraction of natural
> numbers is unnecessary.  Nothing is stopping someone from implementing
> this functionality, and in fact I may do so myself;  however, since such
> functionality is not needed merely for using these numbers, I decided to
> leave it out in order to avoid having to use non-Haskell 2010 extensions
> (especially UndecidableInstances).  In particular, a major motivation
> behind designing the package in this way is to make it more appealing as
> a standard means for representing natural number annotations in order to
> promote interoperability between libraries.
> 
Type level addition doesn't require UndecidableInstances. It only
require TypeFamilies or fundeps. Here is implementation using type
families:

> type family Add n m :: *
>
> type instance Add Zero  Zero           = Zero
> type instance Add Zero (SuccessorTo n) = SuccessorTo n
> type instance Add (SuccessorTo n) m    = SuccessorTo (Add n m)

Standard package is could be somewhat difficult. Standards are
undeniably good but "one size doesn't fit all" rule does apply here.
Your package couldn't be used to represent big numbers. Little real
work has been done on this so it's reasonable to expect progress or
even some breakthough. 

Maybe some generic inteface for conversion of different representation
of natural numbers would be good. Any suggestions

-- 
Alexey Khudyakov <alexey.skladnoy at gmail.com>