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 =

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-260000...

+1 On Tue, Nov 11, 2014 at 9:30 AM, Henning Thielemann < lemming@henning-thielemann.de> wrote:

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 Libraries@haskell.org 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 wrote:

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

-- You received this message because you are subscribed to the Google Groups "haskell-core-libraries" group. To unsubscribe from this group and stop receiving emails from it, send an email to haskell-core-libraries+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

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

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.

er happily On Tue, Nov 11, 2014 at 8:56 AM, Edward Kmett wrote:

+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 wrote:

...

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.

-- You received this message because you are subscribed to the Google Groups "haskell-core-libraries" group. To unsubscribe from this group and stop receiving emails from it, send an email to haskell-core-libraries+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

On Nov 11, 2014, at 2:06 PM, David Feuer 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

On Nov 12, 2014, at 2:16 PM, Iavor Diatchki 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

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 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 Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

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 Libraries@haskell.org 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" mailto:dhelta.diaz@gmail.com> 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 Libraries@haskell.org mailto:Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org mailto:Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org 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 andreas.abel@gu.se http://www2.tcs.ifi.lmu.de/~abel/

On 13/11/14 05:35 PM, Brandon Allbery wrote:

On Thu, Nov 13, 2014 at 5:20 PM, Mario Blažević mailto:mblazevic@stilo.com> 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.

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

I'm neutral on adding Nat or Natural.... seems you math types :-) need to sort out how to handle subtraction.... the rest of us dirty-hands mechanics are fine with the quirky subtract operation on Words... BUT -2 to adding this to Data.Word. This is not the place to add this, for at least two reasons: - Data.Int and Data.Word are the "go to" places for types that correspond closely with what modern hardware supports, and what most interoperable specifications are written to (think file formats, protocols, RFCs, etc....). Nat has none of these properties and is hardly universally agreed upon! - People import Data.Word unqualified all the time - I don't think this type meets the trade-off for adding something into many program's global name space. ​

Hi, On 18 November 2014 16:38, Andres Löh wrote:

FWIW, I'm in favour of:

* not putting this into Data.Word, but rather into Data.Nat or Data.Natural * having default subtraction to be saturated rather than partial * adding a Nat type for bounded naturals as well (even if it's just a synonym for Word)

+1 on all points. 'Data.Nat.Nat' will clash with 'data Nat = Z | S Nat' (which is quite popular), but I think that it's better to call that 'Peano' or something similar. Perhaps we could add 'Peano' to Data.Nat while we're at it?