Announce type-level-natural-number-1.0: Simple, Haskell 2010-compatible type level natural numbers
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. I welcome any feedback that the community has to offer. Cheers, Gregory Crosswhite
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
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/
On Fri, 30 Jul 2010 15:20:55 -0700
John Meacham
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.
Balanced ternary is useful for represeting signed integers. Implementation of next, prev and basic arithmetic operations is not very elegant Some time ago I wrote implementation of type level numbers using binary and balanced ternary encoding. Will upload to hackage soon.
Heh. I was just thinking I needed type level naturals last night at the pub. I wanted to support gcc's vector type extension in jhc http://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html which allow diretly expressing vector operations that use the SIMD features of modern CPUS, I didn't want to pre-create every possible choice so encoding the size as a type level number makes sense. I support complex numbers via a similar higher order type,
data Complex_ :: # -> #
then I can use 'Complex_ Float64_' to get unboxed complex doubles. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/
On Fri, 30 Jul 2010, John Meacham wrote:
Heh. I was just thinking I needed type level naturals last night at the pub.
I thought about type level naturals yesterday when working with HList and found that HList's dependency on TemplateHaskell is quite heavy.
I wanted to support gcc's vector type extension in jhc
http://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html
which allow diretly expressing vector operations that use the SIMD features of modern CPUS, I didn't want to pre-create every possible choice so encoding the size as a type level number makes sense.
The llvm wrapper supports CPU vector data types by decimal type level numbers from the type-level package as phantom type parameters, which I found nice to use. However the whole type level arithmetic is quite slow. Btw. I got to know that there is a difference between Vector computing and SIMD computing, most notably that Vector units (like Altivec and SSE) support vector element shuffling and SIMD machines (like GPUs) do not. http://perilsofparallel.blogspot.com/2008/09/larrabee-vs-nvidia-mimd-vs-simd...
participants (4)
-
Alexey Khudyakov -
Gregory Crosswhite -
Henning Thielemann -
John Meacham