On Fri, 30 Jul 2010 13:28:19 -0700
Gregory Crosswhite
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