Hello, 1. I like the idea of having a `Natual` type similar to `Integer`, so +1 from me. 2. I am a bit worried about the partiality of some of the operations, but I don't see an appealing alternative... I guess we should just throw some informative exceptions. 3. I don't mind where it lives, although `Data.Word` does seem a little odd. 4. On the question about the link with type-level Nats: As Richard points out, with the current implementation the two would be unrelated: type-level nats belong to the kind `Nat`, which is just a lifted empty type called `Nat`. I think it would be possible to modify the implementation, to link the two: when promoting, GHC would promote `Natural` to an empty kind, and we'd modify the type-literals to have kind `Natural` instead of `Nat`. I imagine that should not be too hard to do. From a design point of view, I don't know if this is a good idea, but I have not thought about it. As a data point, we don't do this for kind `Symbol` (i.e., it is not linked in any way `String` or `Text`). -Iavor On Wed, Nov 12, 2014 at 7:46 AM, Richard Eisenberg <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
On Nov 12, 2014, at 2:16 PM, Iavor Diatchki <[hidden email]> wrote: > As Richard points out, with the current implementation the two would be unrelated: type-level nats belong to the kind `Nat`, which is just a lifted empty type called `Nat`. I think it would be possible to modify the implementation, to link the two: when promoting, GHC would promote `Natural` to an empty kind, and we'd modify the type-literals to have kind `Natural` instead of `Nat`. I imagine that should not be too hard to do. From a design point of view, I don't know if this is a good idea, but I have not thought about it. As a data point, we don't do this for kind `Symbol` (i.e., it is not linked in any way `String` or `Text`). I'm a big -1 on this idea. I think we can work toward having more of a unified story of term-level things and type-level things, and every bit of magic that we do like this makes that unified story harder to realize. So, while I agree that implementing Iavor's idea wouldn't be hard today, I would encourage us to wait until we can do this without magic. Richard _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Gershom Bazerman
+0.9 for saturated subtraction. Playing devil's advocate, the downside is that if a user forgets to check the subtraction preconditions, saturated subtraction will silently give the wrong answer instead of calling error. So for a (relatively common?) mistake, the consequences will be worse (exceptions are better than wrong values). However, this is balanced by several use cases for which saturated subtraction is the desired behavior. Furthermore there's no existing code to break, so now is the time to make this choice (it would be easier to go to a partial function in the future than vice versa). John L.
On Thu Nov 13 2014 at 2:17:52 AM Gershom B <[hidden email]> wrote: Let me throw in one key bikeshed to be painted. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
Hrmm. Whichever semantics is chosen as the default, I hope the alternative semantics IS available via a newtype wrapper interface :) On Wed, Nov 12, 2014 at 7:51 PM, John Lato <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
I like this idea. Why not put *both* options in newtype-wrapped interfaces over an underlying version with unchecked subtraction? On Nov 12, 2014 8:24 PM, "Carter Schonwald" <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
...... what would the semantics of unchecked subtraction be? On Wed, Nov 12, 2014 at 8:27 PM, David Feuer <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Iavor Diatchki
Iavor laid out the options nicely, so I'm building off of his response. On Wed, Nov 12, 2014 at 9:16 PM, Iavor Diatchki wrote:
A definite +1 from me, too.
I agree, but see my response to John Lato below.
Agreed with this, too, but I'm not sure of a better place. Would it be worth exporting Integer from Data.Int to have symmetry? Or is that silly? On Thu, Nov 13, 2014 at 2:51 AM, John Lato wrote:
I'm not sure how it would be “easier to go to a partial function” if your code expects saturation. Here's another option: Provide total (or partial) functions by default in the Num and other instances, and provide supplementary partial (total) functions for those who want the other semantics. Regards, Sean _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
indeed. I think the Saturating option should be the newtyped one, and the "expected" one should be the default. Anything else is out of scope for the original proposal on the table and easily a long running bikeshed blood bath. On Thu, Nov 13, 2014 at 1:03 AM, Sean Leather <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Sean Leather-2
On Thu Nov 13 2014 at 2:04:31 PM Sean Leather <[hidden email]> wrote:
Simple. If my code expects saturation, and the semantics change to a partial function, I get an exception and can easily fix it. If my code expects exceptions for invalid subtractions, and the exception path is replaced with a saturating operation, I'll just get incorrect values, which are much more difficult to track down. I think it's important to get the semantics right from the beginning when there's no cost to changing them, so it's worth spending some time discussing the pros and cons here.
That is an option, but it's one that seems rarely taken in Haskell. I think most people would expect alternate semantics via newtypes. It doesn't particularly matter to me how this is resolved, but I do find it slightly odd that so many people seem to be arguing for a partial function as the default in this case. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Gershom Bazerman
On 2014-11-12 at 19:17:21 +0100, Gershom B wrote:
> 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. I'd point out that while for single operations saturated arithmetic seems fine, it leads to less obvious results for compound expression where an intermediate result gets saturated, like in 100 + 20 - 40 => 80 100 + (20 - 40) => 100 (or ⊥ for partial (-)) or (1 - 2) * (10 - 20) => 0 (or ⊥ for partial (-)) . I have to admit I feel a bit uneasy here, and I'd rather get a final ⊥ than a result obtained by continuing the computations with 0s. FWIW, we do already have a precedent of allowing partial functions, like e.g. for quot/Rem/div/mod with a 0-divisor resulting in ⊥ > As a general principle, I think our goal should be to make base more > total, not less. Btw, are we talking only about '(-)' and 'negate'? (e.g. is it ok for 'fromInteger' to diverge for negative input values, or shall it rather map everything negative into '0::Natural'?) > 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. Btw, that paper also argues for "x / 0 = x" instead of throwing a div/0 exception. Should we consider that as well? _______________________________________________ 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 at 10:35:20 +0100, 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 FYI, here's a first draft for its implementation https://phabricator.haskell.org/D473 It currently uses non-saturating arithmetic, but that's not set in stone. A test-suite is in the works; if you notice anything odd in the code, please annotate the patch (click on the line-numbers to create an inline-comment, and don't forget to commit all inline annotations by submitting the comment-form at the bottom of that page) Cheers, hvr _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Sean Leather-2
I am +1 on having Natural in base, I don't really mind the place
(although I also admit that Data.Word seems odd to me).
About subtraction. For the Num instance of Natural, I'd prefer (x - y) where (y > x) to fail with an error call. This is consistent with the behavior we already have for division. The type `(-) :: Natural -> Natural -> Natural` forces us to return a value for any pair of naturals. However, subtraction is not defined for every pair, so it makes sense to me for the function to be partial. That being said, I consider myself an enemy of partial functions (head, tail, and family), and I'd probably prefer to use subtraction with the following type: safeSubtract :: Natural -> Natural -> Maybe Natural With this type, we are not forced to return a value for every pair, returning Nothing instead for those cases where subtraction does not make sense. This is, IMHO, the best way to subtract naturals. Best regards, Daniel Díaz. On 11/13/2014 01:03 AM, Sean Leather
wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
Another approach is to ask "which is larger, and by how much?" to which the answer is Either the Left or the Right. On Nov 13, 2014 11:22 AM, "Daniel Díaz" <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
On 13.11.2014 17:24, David Feuer wrote:
> Another approach is to ask "which is larger, and by how much?" to which > the answer is Either the Left or the Right. Yes, but one would have to have three outcomes: the Left is larger by n, the Right is larger by n, or they are Equal. Otherwise the result for equal nats is a bit arbitrary. (See Conor McBride's Compare type family.) compare m n = LT k ==> m+k+1 = n compare m n = EQ ==> m = n compare m n = GT k ==> m = n+k+1 > > On Nov 13, 2014 11:22 AM, "Daniel Díaz" <[hidden email] > <mailto:[hidden email]>> wrote: > > I am +1 on having Natural in base, I don't really mind the place > (although I also admit that Data.Word seems odd to me). > > About subtraction. For the Num instance of Natural, I'd prefer (x - > y) where (y > x) to fail with an error call. This is > consistent with the behavior we already have for division. The type > `(-):: Natural ->Natural -> Natural` forces us to return > a value for any pair of naturals. However, subtraction is not > defined for every pair, so it makes sense to me for the function > to be partial. > > That being said, I consider myself an enemy of partial functions > (head, tail, and family), and I'd probably prefer to use subtraction > with the following type: > > safeSubtract :: Natural -> Natural -> Maybe Natural > > With this type, we are not forced to return a value for every pair, > returning Nothing instead for those cases where subtraction does not > make > sense. This is, IMHO, the best way to subtract naturals. > > Best regards, > Daniel Díaz. > > On 11/13/2014 01:03 AM, Sean Leather wrote: >> Iavor laid out the options nicely, so I'm building off of his >> response. >> >> On Wed, Nov 12, 2014 at 9:16 PM, Iavor Diatchki wrote: >> >> 1. I like the idea of having a `Natual` type similar to >> `Integer`, so +1 from me. >> >> >> A definite +1 from me, too. >> >> 2. I am a bit worried about the partiality of some of the >> operations, but I don't see an appealing alternative... I >> guess we should just throw some informative exceptions. >> >> >> I agree, but see my response to John Lato below. >> >> 3. I don't mind where it lives, although `Data.Word` does seem >> a little odd. >> >> >> Agreed with this, too, but I'm not sure of a better place. Would >> it be worth exporting Integer from Data.Int to have symmetry? Or >> is that silly? >> >> On Thu, Nov 13, 2014 at 2:51 AM, John Lato wrote: >> >> +0.9 for saturated subtraction. >> Playing devil's advocate, the downside is that if a user >> forgets to check the subtraction preconditions, saturated >> subtraction will silently give the wrong answer instead of >> calling error. So for a (relatively common?) mistake, the >> consequences will be worse (exceptions are better than wrong >> values). >> >> However, this is balanced by several use cases for which >> saturated subtraction is the desired behavior. Furthermore >> there's no existing code to break, so now is the time to make >> this choice (it would be easier to go to a partial function in >> the future than vice versa). >> >> >> I'm not sure how it would be “easier to go to a partial function” >> if your code expects saturation. >> >> Here's another option: Provide total (or partial) functions by >> default in the Num and other instances, and provide supplementary >> partial (total) functions for those who want the other semantics. >> >> Regards, >> Sean >> >> >> _______________________________________________ >> Libraries mailing list >> [hidden email] <mailto:[hidden email]> >> http://www.haskell.org/mailman/listinfo/libraries > > > _______________________________________________ > Libraries mailing list > [hidden email] <mailto:[hidden email]> > http://www.haskell.org/mailman/listinfo/libraries > > > > _______________________________________________ > Libraries mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/libraries > -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden [hidden email] http://www2.tcs.ifi.lmu.de/~abel/ _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
Yes, you're right of course. On Nov 13, 2014 12:06 PM, "Andreas Abel" <[hidden email]> wrote:
On 13.11.2014 17:24, David Feuer wrote: _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Herbert Valerio Riedel
On 14-11-11 04:35 AM, 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...) +1 from me. Regarding the partial vs. saturated negation, I'm in favour of the former. However, there is another option nobody mentioned so far: NaN. I.e., 1 - 2 = NaN 3 + 1 - 2 = 2 3 + (1 - 2) = NaN Could a GMP-based implementation provide such semantics without too much performance loss? If so, this would be my preference. > > 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 Thu, Nov 13, 2014 at 5:20 PM, Mario Blažević <[hidden email]> wrote: Regarding the partial vs. saturated negation, I'm in favour of the former. However, there is another option nobody mentioned so far: NaN NaN is only defined in the context of IEEE floating point; as such, it is not available for this use. brandon s allbery kf8nh sine nomine associates unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
On 13/11/14 05:35 PM, Brandon Allbery wrote:
> On Thu, Nov 13, 2014 at 5:20 PM, Mario Blažević <[hidden email] > <mailto:[hidden email]>> wrote: > > Regarding the partial vs. saturated negation, I'm in favour of the > former. However, there is another option nobody mentioned so far: NaN > > > NaN is only defined in the context of IEEE floating point; as such, it > is not available for this use. I'm aware of the current uses of NaN. I was just suggesting that the same concept could be used for operations on natural values that go out of band. Just like we have isNaN :: RealFloat a => a -> Bool we could add a function isUnnatural :: Natural -> Bool and replace exceptions by an unnatural Natural values... I'm open to an alternative terminology. The important question is whether this approach is feasible for the implementation. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
Nan actually has a point in floating ... point. Here it'd not have any performance benefit and force ME and other Users to do error checking by hand in a needless painful way. Nan on ... nats, just ain Natural. i want simple user friendly error messages. On Thu, Nov 13, 2014 at 10:34 PM, Mario Blažević <[hidden email]> wrote: On 13/11/14 05:35 PM, Brandon Allbery wrote: _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
In reply to this post by Mario Blažević
On 2014-11-13 at 23:20:47 +0100, Mario Blažević wrote:
[...] > Regarding the partial vs. saturated negation, I'm in favour of > the former. However, there is another option nobody mentioned so far: > NaN. I.e., > > 1 - 2 = NaN > 3 + 1 - 2 = 2 > 3 + (1 - 2) = NaN > > Could a GMP-based implementation provide such semantics > without too much performance loss? If so, this would be my preference. Purely from a technical point of view: If you look at how it's implemented right now: https://phabricator.haskell.org/D473 being able to represent a 'not-a-natural' would be possible for the GMP2-backed 'Natural' by adding a 'NatErr#' constructor, i.e. data Natural = NatS# Word# | NatJ# {-# UNPACK #-} !BigNat | NatErr# deriving (Eq,Ord) that, however, would require to add one or two case-distinction to all 'Natural' operations, and we probably shouldn't auto-derive 'Eq'/'Ord' anymore (as it's no longer to be considered a properly ordered set/equivalence relation with that absorbing NatErr# element) However, also the fallback implementation (for when GHC is configured with a the old integer-gmp or the integer-simple backend) which is newtype Natural = Natural Integer would need to become more complex, as the lightweight newtype would be turned into something like data Natural = Natural !Integer | NaturalErr So I'm afraid handling not-a-natural would indeed come at a cost. Cheers, hvr _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries |
Free forum by Nabble | Edit this page |