An additive torsor is?

Surprisingly, there is a page on MathWorld about Torsors but it is empty. Google turned up the following page with a good explanation. http://math.ucr.edu/home/baez/torsors.html

I'd maintain that the difference between two lengths is an entirely different quantity from the length of a list.

(Maybe this is a good example of what the term torsor captures.) Thanks to Aaron for expanding our vocabulary. Jared. -- http://www.updike.org/~jared/ reverse ")-:"

G'day all. Quoting Jared Updike :

Surprisingly, there is a page on MathWorld about Torsors but it is empty. Google turned up the following page with a good explanation.

http://math.ucr.edu/home/baez/torsors.html

Ah, right. So "torsor" is just a short name for "regular group action",which in turn is a short name for "free transitive group action". We discussed these previously in the context of other kinds of difference types: http://www.haskell.org/pipermail/libraries/2005-May/003899.html Cheers, Andrew Bromage

Hello, On 3/23/06, Ben Rudiak-Gould wrote:

Daniel McAllansmith wrote:

...

I can see the domain bounds check would be a problem in theory, but in practice doesn't the type enforce that? Keeping Word positive costs nothing because it just overflows. Wouldn't it be much the same?

If you're planning wraparound semantics then you're better off with Int indexes. Passing an index congruent to -1 mod 2^32 is certainly an error, and (!!) may as well fail immediately rather than try to traverse 2^32-1 list nodes. I think both Int and Word are equally "correct" here, since both are proper supersets of the valid set of indexes. (If you're working with lists so long that Int may not be big enough, you shouldn't trust Word either.)

This need not be the case: Haskell has only positive literals, so there could be a separate class that does not have 'negate' and '(-)' of which natural numbers are an instance. Then overflows would only occur through the 'topEnd' of the number :-). Of course one could still use 'n+k' patterns to decrement naturals in loops. -Iavor

On Fri, 24 Mar 2006, Aaron Denney wrote:

On 2006-03-24, Daniel McAllansmith wrote:

...

Unless I've missed it, there is no typeclass for positive integers in GHC. Is there any particular reason it doesn't exist?

The number of useable operations is small, and checks for leaving the domain would have to be done all the time. It basically doesn't buy anything.

A new type, say Cardinal as in Modula, would document for the user of a function that only non-negative numbers are allowed and the function writer can be sure, that only non-negative numbers are passed. Today function writers have to check explicitly for negative numbers, when they are not wanted. With a Cardinal type some of these checks can be dropped because of the static guarantee that Cardinals are never negative. Further on think of QuickCheck: A Cardinal type with an Arbitrary instance would save us the (>=0) condition and it would reduce the number of tests that must be skipped because of non-fulfilled conditions. Because I was confronted with adding positivity checks to QuickCheck properties quite frequently, I finally wrote wrappers newtype Cardinal = Cardinal Integer deriving (Show, Read, Eq, Ord, Ix) newtype Card = Card Int deriving (Show, Read, Eq, Ord, Ix) in order to simplify such checks. Since the pros and cons of new types are true for every number type, the discussion whether Cardinal should be supported or not ends up with the question how often it can be used. When I look through my Modula programs I encounter CARDINAL quite often, so yes, it seems to be useful. Inductive definitions of functions of integers need a base case - which is often zero. That is such functions are intended for Cardinals rather than Integers. The (n+k) pattern are often defended because of its use in inductive definitions. So I claim that Cardinals are at least as important as (n+k) patterns. :-)

On 2006-03-24, Henning Thielemann wrote:

On Fri, 24 Mar 2006, Aaron Denney wrote:

...

On 2006-03-24, Daniel McAllansmith wrote:

...

Unless I've missed it, there is no typeclass for positive integers in GHC. Is there any particular reason it doesn't exist?

The number of useable operations is small, and checks for leaving the domain would have to be done all the time. It basically doesn't buy anything.

A new type, say Cardinal as in Modula, would document for the user of a function that only non-negative numbers are allowed and the function writer can be sure, that only non-negative numbers are passed. Today function writers have to check explicitly for negative numbers, when they are not wanted. With a Cardinal type some of these checks can be dropped because of the static guarantee that Cardinals are never negative.

As long as the constructors aren't exposed, and then the checks get pushed into the injection function. Which really doesn't give us "static safety", but does let us push the discovery earlier, so may still be useful. And indexing still needs to check for overflows.

Further on think of QuickCheck: A Cardinal type with an Arbitrary instance would save us the (>=0) condition

True.

The (n+k) pattern are often defended because of its use in inductive definitions. So I claim that Cardinals are at least as important as (n+k) patterns. :-)

And neither need to be in the language. :) Basically, my big objection is that it's hard to define many useful operations on them that are statically safe. Any definition of Num a for instance leaves a whole bunch of unsafe methods, or just plain inapplicable methods, such as "negate". Now granted, the numeric hierarchy should be broken up a bit (hmm, I should finish my strawman proposal for Haskell'), but even then I see problems. -- Aaron Denney -><-

On 2006-03-24, Henning Thielemann wrote:

On Fri, 24 Mar 2006, Aaron Denney wrote:

...

Basically, my big objection is that it's hard to define many useful operations on them that are statically safe.

Why not defining the Torsor class you suggested?

Torsor is not quite the right word -- it's just that one of the contexts for non-negative numbers is very similar to one fairly standard example of torsors -- pointers and offsets.

...

Now granted, the numeric hierarchy should be broken up a bit (hmm, I should finish my strawman proposal for Haskell'), but even then I see problems.

Hm, is there something going on?

A strawman proposal, not yet posted anywhere.

Without breaking compatibility? But class instances become invalid if the hierarchy is modified.

No, compatibility will be broken. Hopefully not for most uses -- I don't think most people define new instances, and those that do will be able to do so more reasonably, so hopefully wouldn't mind.

If there is some progress towards a refined numeric class hierarchy I want to point again to http://cvs.haskell.org/darcs/numericprelude/ http://cvs.haskell.org/darcs/numericprelude/src/Algebra/Core.lhs I hope I don't annoy you. :-)

Not at all. That is one of the things I looked at a while ago, that has inspired a lot of my decisions -- but I'm more willing to rename things that I think have silly names. And there are a few minor details, like allowing only for euclidean domains rather than principal ideal domains. I will probably actually put two proposals up, with one allowing more generality via MPTCs and FDs (which I truly hope make it into the standard). -- Aaron Denney -><-

On Fri, Mar 24, 2006 at 06:54:54PM +0000, Aaron Denney wrote:

...

Without breaking compatibility? But class instances become invalid if the hierarchy is modified.

No, compatibility will be broken. Hopefully not for most uses -- I don't think most people define new instances, and those that do will be able to do so more reasonably, so hopefully wouldn't mind.

The problem isn't with creating instances, it is with using the classes at all. well, in interfaces you are going to end up with some specific class or another concretely mentioned in your type signatures, which means you can't interact with code that only knows about the alternate class. like genericLength :: Integral a => [b] -> a if you have a different 'Integral' you can't call genericLength with it, or anything built up on genericLength. basically there would be no way for 'new' and 'old' polymorphic code to interact. the inability to evolve the class hierarchy is a serious issue, enough that it very well could be impractical for haskell' unless something like class aliases were widely adopted. John -- John Meacham - ⑆repetae.net⑆john⑈

On 2006-03-27, Dylan Thurston wrote:

--===============0906829955== Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="3V7upXqbjpZ4EhLz" Content-Disposition: inline

--3V7upXqbjpZ4EhLz Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: quoted-printable

On Mon, Mar 27, 2006 at 05:02:20AM -0800, John Meacham wrote:

...

well, in interfaces you are going to end up with some specific class or another concretely mentioned in your type signatures, which means you can't interact with code that only knows about the alternate class. like =20 genericLength :: Integral a =3D> [b] -> a =20 if you have a different 'Integral' you can't call genericLength with it, or anything built up on genericLength. basically there would be no way for 'new' and 'old' polymorphic code to interact.=20

I think the idea would be that the source for genericLength would compile using either class hierarchy with no change. For the case of genericLength, this is true for the proposed alternate prelude Hennig Theilemann pointed to. It would be mostly true in general for that proposal, with the exception that you would sometimes need to add Show or Eq instances.

Right.

...

the inability to evolve the class hierarchy is a serious issue, enough that it very well could be impractical for haskell' unless something like class aliases were widely adopted.

I think that as long as you're not defining classes source compatibility would not be hard. Of course you couldn't hope to link code written with one hierarchy against another.

Wouldn't instance declaration also be problematic? (And yes, we desperately need something like class aliases.) -- Aaron Denney -><-

On 2006-04-02, ihope wrote:

On 3/29/06, Aaron Denney wrote:

...

(And yes, we desperately need something like class aliases.)

You mean like this?

Not quite, I meant something like John Meacham's proposal: http://repetae.net/john/recent/out/classalias.html -- Aaron Denney -><-

On 3/24/06, Henning Thielemann wrote:

A new type, say Cardinal as in Modula, would document for the user of a function that only non-negative numbers are allowed and the function writer can be sure, that only non-negative numbers are passed.

...

newtype Cardinal = Cardinal Integer deriving (Show, Read, Eq, Ord, Ix) newtype Card = Card Int deriving (Show, Read, Eq, Ord, Ix)

Has anybody tried to implement arbitrary- and machine-size natural numbers (Cardinal and Card, respectively) in GHC using unboxed types? It should be just a matter of tweaking Int, Integer and Word a bit.

On Fri, 24 Mar 2006, Malcolm Wallace wrote:

Daniel McAllansmith wrote:

...

Unless I've missed it, there is no typeclass for positive integers in GHC. Is there any particular reason it doesn't exist?

Also, it seems Word would be a far better type in the likes of (!!), length, etc. Is it just tradition that resulted in the use of Int?

There is a good argument that what you really want here is the lazy infinite natural numbers. Think Peano:

data Natural = Zero | Succ Natural

The clear correspondance between lazy lists and the size/index of a lazy list makes this type fairly compelling. It can be jolly useful, particularly with infinite streams, to be able to compute (length xs > n) without forcing the evaluation of the list to more than n places.

Fortunately there are already List functions like genericLength and genericTake, which can handle such a number type. Shouldn't be Peano numbers part of the standard libraries?

On Friday 24 March 2006 23:29, Malcolm Wallace wrote:

Daniel McAllansmith wrote:

...

Unless I've missed it, there is no typeclass for positive integers in GHC. Is there any particular reason it doesn't exist?

Also, it seems Word would be a far better type in the likes of (!!), length, etc. Is it just tradition that resulted in the use of Int?

There is a good argument that what you really want here is the lazy infinite natural numbers. Think Peano:

data Natural = Zero | Succ Natural

The clear correspondance between lazy lists and the size/index of a lazy list makes this type fairly compelling. It can be jolly useful, particularly with infinite streams, to be able to compute (length xs > n) without forcing the evaluation of the list to more than n places.

Of course, if the naturals were actually represented in Peano (unary) form, that would be somewhat inefficient, but there are various strategies that can be used to make the representation smaller whilst retaining their nice properties.

I was thinking about several things in this thread, torsors, overflow semantics, bounds checking... I wonder if there would be any merit in being able to define constrained subsets of integers and the semantics when/if they overflow. For example, take UNIX nice levels -20 to 19. You could have data ConstrainedInteger = CI {distToMax :: Natural, distToMin :: Natural} this would ensure only the 40 integers can be represented. Then you could have _something_ that defined what happened on overflow, whether it wraps, reflects, errors, truncates or whatever. When it comes to compile, or source preprocessing, time these numbers could be realigned to a primitive Int or Word representation of suitable size and have the appropriate overflow code written in. And, in the case of error or wrap overflow semantics on a set of the right size, the overflow checks could be disabled, like other assertions, at runtime. Daniel

On Mar 26, 2006, at 4:35 PM, Daniel McAllansmith wrote:

[Discussion of positive integers and Words]

I was thinking about several things in this thread, torsors, overflow semantics, bounds checking... I wonder if there would be any merit in being able to define constrained subsets of integers and the semantics when/if they overflow.

Oddly, I've just finished coding this up, with type-level bounds (represented by type-level ints). It's a big pile of modules on top of John Meacham's type-level Nats library, which add type-level Ints (as non-normalized Nat pairs), unknown endpoints (permitting Integer to fit in the same framework), and the actual bounded ints themselves. Naturally, I needed to define my own versions of the functionality in Eq, Ord, and Num. These resolve statically as much as possible (including some possibly dubious behavior with singleton intervals). That said, I don't try to do everything at the type level---it became too tiring, with not enough plausible benefit. Any and all: Drop me a line if you are interested, it's a stack of 3-4 modules and at best half-baked. I'd just gotten a mostly- complete version. -Jan-Willem Maessen

Doesn't Ada have constrained number types which have similar behaviour?

Yes. Just for comparison, the behaviour of the Ada number is to throw an exception at runtime if a number overflows its bounds. If these checks can be eliminated statically, then they are. If an operation will always give a runtime error then this is given as a warning at compile time. Thanks Neil