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/