Hello CLC et al.,
I hereby suggest to add a type for encoding term-level naturals data Natural = <opaque/hidden> deriving (...the usual standard classes...) to `base:Data.Word` module Motivation ========== - GHC 7.10 is planned to ship with integer-gmp2[2] as its default `Integer` lib, whose low-level primitives are based on *unsigned* BigNums. And 'Natural' type for integer-gmp2 can be implemented directly w/o the overhead of wrapping an `Integer` via data Natural = NatS# Word# | NatJ# !PrimBigNat# as well as having a twice as large domain handled via the small-word constructor and thus avoiding FFI calls into GMP. - GHC/`base` already provides type-level naturals, but no term-level naturals - Remove the asymmetry of having an unbounded signed `Integer` but no unbounded /unsigned/ integral type. Also, `Data.Word` has been carrying the following note[1] for some time now: > It would be very natural to add a type Natural providing an > unbounded size unsigned integer, just as Integer provides unbounded > size signed integers. We do not do that yet since there is no > demand for it. Discussion period: ~10 days (GHC 7.10 RC freeze is scheduled for Nov 21st) Cheers, hvr [1]: http://hackage.haskell.org/package/base-4.7.0.1/docs/Data-Word.html#g:3 [2]: https://phabricator.haskell.org/D82 https://ghc.haskell.org/trac/ghc/wiki/Design/IntegerGmp2 _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
+1, undoubtedly.
-- Felipe. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries signature.asc (836 bytes) Download Attachment |
In reply to this post by Herbert Valerio Riedel
On Tue, 11 Nov 2014, Herbert Valerio Riedel wrote: > Hello CLC et al., > > I hereby suggest to add a type for encoding term-level naturals > > data Natural = <opaque/hidden> > deriving (...the usual standard classes...) > > to `base:Data.Word` module This type is useful, no doubt. But so far Data.Word (and Data.Int) are modules for fixed size machine oriented integer types. Would be nice to have Natural located where Integer is. Unfortunately, so far Integer is only exported by Prelude and GHC.Integer. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Herbert Valerio Riedel
What would the semantics of subtraction be for this? I'm assuming there would be a `Num` instance for `Natural`.
Richard On Nov 11, 2014, at 4:35 AM, Herbert Valerio Riedel <[hidden email]> wrote: > Hello CLC et al., > > I hereby suggest to add a type for encoding term-level naturals > > data Natural = <opaque/hidden> > deriving (...the usual standard classes...) > > to `base:Data.Word` module > > Motivation > ========== > > - GHC 7.10 is planned to ship with integer-gmp2[2] as its default > `Integer` lib, whose low-level primitives are based on *unsigned* > BigNums. And 'Natural' type for integer-gmp2 can be implemented > directly w/o the overhead of wrapping an `Integer` via > > data Natural = NatS# Word# | NatJ# !PrimBigNat# > > as well as having a twice as large domain handled via the small-word > constructor and thus avoiding FFI calls into GMP. > > - GHC/`base` already provides type-level naturals, but no term-level > naturals > > - Remove the asymmetry of having an unbounded signed `Integer` but no > unbounded /unsigned/ integral type. > > Also, `Data.Word` has been carrying the following note[1] for some > time now: > >> It would be very natural to add a type Natural providing an >> unbounded size unsigned integer, just as Integer provides unbounded >> size signed integers. We do not do that yet since there is no >> demand for it. > > > > Discussion period: ~10 days (GHC 7.10 RC freeze is scheduled for Nov 21st) > > Cheers, > hvr > > [1]: http://hackage.haskell.org/package/base-4.7.0.1/docs/Data-Word.html#g:3 > > [2]: https://phabricator.haskell.org/D82 > https://ghc.haskell.org/trac/ghc/wiki/Design/IntegerGmp2 > _______________________________________________ > Libraries mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
On 2014-11-11 at 14:32:47 +0100, Richard Eisenberg wrote:
> What would the semantics of subtraction be for this? I'm assuming > there would be a `Num` instance for `Natural`. It wouldn't be total, and 'throw (Underflow :: ArithException)' if the result would fall outside the non-negative domain. This is similiar to how e.g. http://hackage.haskell.org/package/nats-0.2/docs/Numeric-Natural.html handles out-of-domain subtraction results. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
+1 from me. I'd happy hack up 'nats/semigroups' to use a standard version if it was available. On Tue, Nov 11, 2014 at 8:51 AM, Herbert Valerio Riedel <[hidden email]> wrote: On 2014-11-11 at 14:32:47 +0100, Richard Eisenberg wrote: _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
er happily On Tue, Nov 11, 2014 at 8:56 AM, Edward Kmett <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Henning Thielemann
Hello Henning,
On 2014-11-11 at 14:11:25 +0100, Henning Thielemann wrote: >> I hereby suggest to add a type for encoding term-level naturals >> >> data Natural = <opaque/hidden> >> deriving (...the usual standard classes...) >> >> to `base:Data.Word` module > > This type is useful, no doubt. But so far Data.Word (and Data.Int) are > modules for fixed size machine oriented integer types. Looking at the Haskell Report 2010 description of "Data.Word"[1] there is no clear indication that an unbounded `Natural` would be out of scope for "Data.Word" IMHO: ,---- | 23.1 Unsigned integral types | | This module provides unsigned integer types of unspecified width (Word) | and fixed widths (Word8, Word16, Word32 and Word64). All arithmetic is | performed modulo 2^n, where n is the number of bits in the type. | | ... `---- > Would be nice to have Natural located where Integer is. Unfortunately, > so far Integer is only exported by Prelude and GHC.Integer. There's a couple of alternatives I can think of rightaway: 1) Interpret "Data.Word" to really mean "unsigned integral types" as as the Haskell Report's heading seems to suggest 2) Export 'Natural' from 'Prelude' (we recently exported 'Word' from the 'Prelude' as well, so...) 3) Refrain from touching any Haskell Report controlled module, and just place the new type into a new GHC-specific module "GHC.Natural", if variant 1) and/or 2) fail to reach consensus at this time. Cheers, hvr [1]: https://www.haskell.org/onlinereport/haskell2010/haskellch23.html#x31-26000023 _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
On Tue, 11 Nov 2014, Herbert Valerio Riedel wrote: > ,---- > | 23.1 Unsigned integral types > | > | This module provides unsigned integer types of unspecified width (Word) > | and fixed widths (Word8, Word16, Word32 and Word64). All arithmetic is > | performed modulo 2^n, where n is the number of bits in the type. > | > | ... > `---- "Number of bits in the type" suggests, that the number of bits depends only on the type, which is not true for Natural (and Integer), right? _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
+1
On Tue, Nov 11, 2014 at 9:30 AM, Henning Thielemann <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Herbert Valerio Riedel
errr, I meant +1 here On Tue, Nov 11, 2014 at 4:35 AM, Herbert Valerio Riedel <[hidden email]> wrote: Hello CLC et al., _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Henning Thielemann
On 2014-11-11 at 15:30:49 +0100, Henning Thielemann wrote:
>> ,---- >> | 23.1 Unsigned integral types >> | >> | This module provides unsigned integer types of unspecified width (Word) >> | and fixed widths (Word8, Word16, Word32 and Word64). All arithmetic is >> | performed modulo 2^n, where n is the number of bits in the type. >> | >> | ... >> `---- > > "Number of bits in the type" suggests, that the number of bits depends > only on the type, which is not true for Natural (and Integer), right? Yeah, if that `n` is meant to mean a finite natural value, then you've got a point here. Otoh, one could maybe consider 'Natural' following modulo arithmetic 2^n with an infinite number `n` of bits, and hence can never arithmetically overflow. If an operation would, however, cause an underflow it simply 'throw (Underflows :: ArithException)'. However, one could extend the Data.Word documentation to note that 'Natural' represents an asymptotic limit/exception here with respect to modulo 2^n arithmetic... :-) Cheers, hvr _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
It makes sense to just re-export it from Data.Word, narrow readings of the wording aside. Words can, after all, be changed and don't necessarily represent some grand insight from the past. After all this is the module where the note about how we could add Natural in the first place lives. On Tue, Nov 11, 2014 at 10:01 AM, Herbert Valerio Riedel <[hidden email]> wrote: On 2014-11-11 at 15:30:49 +0100, Henning Thielemann wrote: _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Herbert Valerio Riedel
On 2014-11-11 10:35, Herbert Valerio Riedel wrote:
> Hello CLC et al., > > I hereby suggest to add a type for encoding term-level naturals > > data Natural = <opaque/hidden> > deriving (...the usual standard classes...) > > to `base:Data.Word` module > +1, not that I've been particularly *missing* it as such, but it does make sense in this context. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Herbert Valerio Riedel
I'm definitely in favor of this idea. How (if at all) would you like these term-level natural numbers to relate to the type-level ones? On Tue, Nov 11, 2014 at 4:35 AM, Herbert Valerio Riedel <[hidden email]> wrote: Hello CLC et al., _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Herbert Valerio Riedel
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1 > "add unsigned Integer" +1 from the "I've been missing this" department. David/quchen -----BEGIN PGP SIGNATURE----- Version: GnuPG v1 iQEcBAEBAgAGBQJUY0AGAAoJELrQsaT5WQUsRUQIAKH8iSE8YpYDf337oPER0+QC V35Jr+Lc1WKtU/Yil5Ps124BTtwxDzFvcJliFNl8FQbm6oM6aqUIoVR6YQ7AR93U XseojL6R+qiYlj3pf+yQnJbgUeg+ab+iyFVhRtO4mUhoYawC8nxYU3kUfkdu6cSt lcCb8kUI/V/UpRy2//yp6rNeYp0x1wkZa5ug7PuQ0F6HsST8ymn3ZlIPH4OTWhi+ yWrqUWUi4C6tnTWrROFeGDWaAfdKy1jtF1YNinFAm/wfxMGrCSLccJZhRrjZzXap 2rKfPolStx9inupi6mD7oXedr4GzxI7zgiQiGi+uMfhJD6yf6eIcFadUMT0W5UE= =xQbU -----END PGP SIGNATURE----- _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Henning Thielemann
On 11/11/14 08:11, Henning Thielemann wrote:
> > > On Tue, 11 Nov 2014, Herbert Valerio Riedel wrote: > >> Hello CLC et al., >> >> I hereby suggest to add a type for encoding term-level naturals >> >> data Natural = <opaque/hidden> >> deriving (...the usual standard classes...) >> >> to `base:Data.Word` module > > This type is useful, no doubt. But so far Data.Word (and Data.Int) are > modules for fixed size machine oriented integer types. Would be nice to > have Natural located where Integer is. Unfortunately, so far Integer is > only exported by Prelude and GHC.Integer. Yeah, having Natural in Data.Word feels unnatural to me. Roman _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
Herbert Valerio Riedel wrote:
>> I hereby suggest to add a type for encoding term-level naturals... >> to `base:Data.Word` module +1 because Edward, who is the current leading purveyor of term-level nats, is in favor. Roman Cheplyaka wrote: > Yeah, having Natural in Data.Word feels unnatural to me. Agreed. I'm not sure what the solution is though. I'd be in favor if someone comes up with something decent. *However* I'd be strongly opposed to letting any kind of bikeshedding getting in the way of Herbert's proposal. Thanks, Yitz _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by David Feuer
On Nov 11, 2014, at 2:06 PM, David Feuer <[hidden email]> wrote: > How (if at all) would you like these term-level natural numbers to relate to the type-level ones? Not at all. It's my belief that there is exists some moderately remote future (2-3 years) in which all datatypes -- including ones with unboxed fields -- will be promotable. At that point, this new `Natural` will promote, too. That future may also contain overloaded numeric literals in types, in which case things would just work. The only problem would be that this `Natural` doesn't have the right inductive structure to reason about in types, but it's no worse than today's `Nat`s. My work for the next few years is to make that future a reality. :) Richard _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Herbert Valerio Riedel
Let me throw in one key bikeshed to be painted.
I don't like the fact that subtraction on naturals is a partial operation as proposed. I would much prefer saturated subtraction where for y > x, x - y = 0. This prior discussion on -cafe tends towards such a definition as being 'universally better' https://www.haskell.org/pipermail/haskell-cafe/2011-March/090265.html Here is my motivation for saturated subtraction: On all non-bottom calculations, it agrees. On calculations that are bottom under partial subtraction, it nonetheless gives a mathematically meaningful and useful result in a coherent way. As a general principle, I think our goal should be to make base more total, not less. The arguments cited in the thread from Runciman's "What About the Natural Numbers" (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.3442) are also fairly compelling in this regard. -g > Herbert Valerio Riedel wrote: >>> I hereby suggest to add a type for encoding term-level naturals... >>> to `base:Data.Word` module > > +1 > > because Edward, who is the current leading purveyor of term-level > nats, is in favor. > > Roman Cheplyaka wrote: >> Yeah, having Natural in Data.Word feels unnatural to me. > > Agreed. I'm not sure what the solution is though. I'd be in > favor if someone comes up with something decent. > *However* > I'd be strongly opposed to letting any kind of bikeshedding > getting in the way of Herbert's proposal. > > Thanks, > Yitz Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
Free forum by Nabble | Edit this page |