[Haskell-cafe] Announce type-level-natural-number-1.0: Simple,
Haskell 2010-compatible type level natural numbers
john at repetae.net
Fri Jul 30 18:20:55 EDT 2010
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
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
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/
More information about the Haskell-Cafe