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

[John Meacham]

On Sat, Jul 31, 2010 at 01:32:50AM +0400, Alexey Khudyakov wrote:
> > 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:

FunDeps also require MPTCs. I am becoming a huge fan of type
families/associated types. There is a fairly good chance jhc will
support them well before or even instead of MPTCs.


> > 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. 

I thought there was some elegant way to express type level numbers
using balanced ternary, but I can't find a reference to it at the
moment.


        John

-- 
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/