Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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:
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
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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.
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.
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'
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.
> 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
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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:
+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.
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'
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.
> 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
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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:
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:
+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.
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'
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.
> 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
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
...... what would the semantics of unchecked subtraction be?
On Wed, Nov 12, 2014 at 8:27 PM, David Feuer <[hidden email]> wrote:
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:
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:
+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.
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'
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.
> 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
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.
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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:
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.
On Thu Nov 13 2014 at 2:04:31 PM Sean Leather <[hidden email]> wrote:
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.
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.
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.
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.
> 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
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'?)
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
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)
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:
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.
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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:
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:
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.
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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:
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
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:
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.
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 >
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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.
Re: PROPOSAL: Add 'Natural' type to base:Data.Word
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:
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.
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.
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.
Locked
