Re: [Haskell-cafe] ordNub

newer
Re; ordNub

older
Negable constraints on boolean...

oleg＠okmij.org

1 Jan 2015 1 Jan '15

8:58 a.m.

Tom Ellis wrote:

...

Is there a type with an Eq instance for which on Ord instance could not also be provided (i.e. I'm interested in Clark's "converse")?

Of course. One of the very many examples is Complex. One can say we can compare complex numbers, by their absolute value. That is true; however we end up in a position where compare x y returns EQ but x==y returns False. In general, Ord represents total order. There are many structures on which total order cannot be established. Take nodes in the tree, the Tree data type. One can compare nodes by taking a parent to be less than any of its children. But then two brothers are not comparable. Searching for "partial orders" and pre-orders gives many more examples.

Show replies by date

Tom Ellis

1 Jan 1 Jan

9:04 a.m.

New subject: ordNub

On Thu, Jan 01, 2015 at 08:58:35AM -0500, oleg@okmij.org wrote:

...

Tom Ellis wrote:

...
Is there a type with an Eq instance for which on Ord instance could not also be provided (i.e. I'm interested in Clark's "converse")?

Of course. One of the very many examples is Complex. One can say we can compare complex numbers, by their absolute value. That is true; however we end up in a position where compare x y returns EQ but x==y returns False.

I don't understand your objection. `Complex a` isomorphic to `(a, a)` which can be totally ordered. (The complex field cannot be given a total order *compatible with the field structure*, but that's not relevant to my question.)

...

In general, Ord represents total order. There are many structures on which total order cannot be established. Take nodes in the tree, the Tree data type. One can compare nodes by taking a parent to be less than any of its children. But then two brothers are not comparable. Searching for "partial orders" and pre-orders gives many more examples.

I think you may be missing the intent of my question. I am merely asking whether there is a type which supports a (law abiding) Eq instance that cannot support a (law abiding) Ord instance. Whether that Ord instance is compatible with additional structures on that type is beside the point. Tom

Atze van der Ploeg

9:12 a.m.

New subject: ordNub

Instance Ord a where _ <= _ = True Is law abiding for any type. So there is no type that cannot support a law abiding Ord instance. On Jan 1, 2015 3:04 PM, "Tom Ellis" < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

...

On Thu, Jan 01, 2015 at 08:58:35AM -0500, oleg@okmij.org wrote:

...
Tom Ellis wrote:

...
Is there a type with an Eq instance for which on Ord instance could not also be provided (i.e. I'm interested in Clark's "converse")?

Of course. One of the very many examples is Complex. One can say we can compare complex numbers, by their absolute value. That is true; however we end up in a position where compare x y returns EQ but x==y returns False.

I don't understand your objection. `Complex a` isomorphic to `(a, a)` which can be totally ordered. (The complex field cannot be given a total order *compatible with the field structure*, but that's not relevant to my question.)

...
In general, Ord represents total order. There are many structures on which total order cannot be established. Take nodes in the tree, the Tree data type. One can compare nodes by taking a parent to be less than any of its children. But then two brothers are not comparable. Searching for "partial orders" and pre-orders gives many more examples.

I think you may be missing the intent of my question. I am merely asking whether there is a type which supports a (law abiding) Eq instance that cannot support a (law abiding) Ord instance. Whether that Ord instance is compatible with additional structures on that type is beside the point.

Tom _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Tom Ellis

9:14 a.m.

New subject: ordNub

On Thu, Jan 01, 2015 at 03:12:15PM +0100, Atze van der Ploeg wrote:

...

Instance Ord a where _ <= _ = True

Is law abiding for any type. So there is no type that cannot support a law abiding Ord instance.

So let me clarify that I want (<=) to be a total order in the sense that it is * reflexive * symmetric * transitive and `(x <= y) && (y <= x)` implies that `x == y`. Tom

Atze van der Ploeg

9:17 a.m.

New subject: ordNub

Taking Instance Eq a where _ == _ = True Then it has all the properties you mentoined On Jan 1, 2015 3:14 PM, "Tom Ellis" < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

...

On Thu, Jan 01, 2015 at 03:12:15PM +0100, Atze van der Ploeg wrote:

...
Instance Ord a where _ <= _ = True

Is law abiding for any type. So there is no type that cannot support a law abiding Ord instance.

So let me clarify that I want (<=) to be a total order in the sense that it is

* reflexive * symmetric * transitive

and `(x <= y) && (y <= x)` implies that `x == y`.

Tom _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Tom Ellis

9:19 a.m.

New subject: ordNub

On Thu, Jan 01, 2015 at 03:17:13PM +0100, Atze van der Ploeg wrote:

...

Taking

Instance Eq a where _ == _ = True

Then it has all the properties you mentoined

Right, hence my latest clarification that "Futhermore I want (==) to be at least as fine-grained as extensional equivalence.".

Atze van der Ploeg

9:22 a.m.

New subject: ordNub

...

i want it to be at least as fine grained as extensional equivalence

Then see Oleg's comment or am i missing something here? On Jan 1, 2015 3:19 PM, "Tom Ellis" < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

...

On Thu, Jan 01, 2015 at 03:17:13PM +0100, Atze van der Ploeg wrote:

...
Taking

Instance Eq a where _ == _ = True

Then it has all the properties you mentoined

Right, hence my latest clarification that "Futhermore I want (==) to be at least as fine-grained as extensional equivalence.". _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Tom Ellis

9:26 a.m.

New subject: ordNub

On Thu, Jan 01, 2015 at 03:22:55PM +0100, Atze van der Ploeg wrote:

...

...
i want it to be at least as fine grained as extensional equivalence

Then see Oleg's comment or am i missing something here?

Perhaps you could explain Oleg's comment. I don't understand it.

Atze van der Ploeg

9:37 a.m.

New subject: ordNub

Your question is if I understand correctly, whether we can think of a type that has a law abiding Eq instance that gives equality as fine grained as extensional equality (meaning structural equality?) but for which no law abing instance of Ord can be given such that a <= b && a >= b ==> a == b This boils down to the question whether on each set with an equality relation defined on it a total ordering (consistent with the equality relation) can also be defined. One counterexample is the complex numbers. Does that answer your question? Cheers! On Jan 1, 2015 3:27 PM, "Tom Ellis" < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

...

On Thu, Jan 01, 2015 at 03:22:55PM +0100, Atze van der Ploeg wrote:

...
...
i want it to be at least as fine grained as extensional equivalence

Then see Oleg's comment or am i missing something here?

Perhaps you could explain Oleg's comment. I don't understand it. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Tom Ellis

9:39 a.m.

New subject: ordNub

On Thu, Jan 01, 2015 at 03:37:09PM +0100, Atze van der Ploeg wrote:

...

This boils down to the question whether on each set with an equality relation defined on it a total ordering (consistent with the equality relation) can also be defined.

I agree with the essence of this restatement.

...

One counterexample is the complex numbers.

This is what I don't understand. The complex numbers can be totally ordered. (Not in a way compatible with the field structure, but that's beside the point).

Atze van der Ploeg

9:52 a.m.

New subject: ordNub

If we do not require that (a <= b) && (a >= b) ==> a == b (where <= is from the total ordering and == is from the equality relation) then it is trivial, take the total ordering forall x y. x <= y that i mentioned earlier. So the compatiblity with equality (you say field structure) is not besides the point, in fact antisymmetry means that the ordering corresponds to the equality relation. Clear now or did I misunderstand? Cheers 2015-01-01 15:39 GMT+01:00 Tom Ellis < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk>:

...

On Thu, Jan 01, 2015 at 03:37:09PM +0100, Atze van der Ploeg wrote:

...
This boils down to the question whether on each set with an equality relation defined on it a total ordering (consistent with the equality relation) can also be defined.

I agree with the essence of this restatement.

...
One counterexample is the complex numbers.

This is what I don't understand. The complex numbers can be totally ordered. (Not in a way compatible with the field structure, but that's beside the point). _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Tom Ellis

10:01 a.m.

New subject: ordNub

On Thu, Jan 01, 2015 at 03:52:26PM +0100, Atze van der Ploeg wrote:

...

If we do not require that (a <= b) && (a >= b) ==> a == b (where <= is from the total ordering and == is from the equality relation) then it is trivial, take the total ordering forall x y. x <= y that i mentioned earlier.

So the compatiblity with equality (you say field structure) is not besides the point, in fact antisymmetry means that the ordering corresponds to the equality relation.

Clear now or did I misunderstand?

Here is my proposed equality and ordering on the complex numbers: data Complex = Complex (Double, Double) deriving (Eq, Ord) Does this violate any of my requested conditions?

Atze van der Ploeg

10:06 a.m.

New subject: ordNub

Nope you're right. Indeed uncompatible with the field structure. Now I'm confused :) I now understand your question, but do not immediately know the answer. Anyone? On Jan 1, 2015 4:02 PM, "Tom Ellis" < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

...

...
If we do not require that (a <= b) && (a >= b) ==> a == b (where <= is from the total ordering and == is from the equality relation) then it is trivial, take the total ordering forall x y. x <= y that i mentioned earlier.

So the compatiblity with equality (you say field structure) is not besides the point, in fact antisymmetry means that the ordering corresponds to

On Thu, Jan 01, 2015 at 03:52:26PM +0100, Atze van der Ploeg wrote: the

...
equality relation.

Clear now or did I misunderstand?

Here is my proposed equality and ordering on the complex numbers:

data Complex = Complex (Double, Double) deriving (Eq, Ord)

Does this violate any of my requested conditions? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Atze van der Ploeg

10:31 a.m.

New subject: ordNub

...

(That said, I don't understand why this discussion is relevant at all. The fact that the ordering exists doesn't mean that one would want to declare the Ord instance, like with complex numbers.)

It's not relevant, it's just an intellectual exercise. For any set with a equality relation there exists a total order relation on that set consistent with the equality relation. The question is then whether there exists a set with a computable equality relation such that there is no computable total order. I think the following computable function shows that it is always possible (it chooses an order during queries): Maintain a table, initially emtpy As soon as (a <= b) is requested, see if a and b are already in the table (using the computatble equality function) , if so, use their ordering in the table. If an element is not in the table, add it. Hence the table gives a consistent total order (it depends on which ordering queries are requested, but that is not relevant?) 2015-01-01 16:06 GMT+01:00 Atze van der Ploeg :

...

Nope you're right. Indeed uncompatible with the field structure. Now I'm confused :)

I now understand your question, but do not immediately know the answer. Anyone? On Jan 1, 2015 4:02 PM, "Tom Ellis" < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

...
...
If we do not require that (a <= b) && (a >= b) ==> a == b (where <= is from the total ordering and == is from the equality relation) then it is trivial, take the total ordering forall x y. x <= y that i mentioned earlier.

So the compatiblity with equality (you say field structure) is not besides the point, in fact antisymmetry means that the ordering corresponds to

On Thu, Jan 01, 2015 at 03:52:26PM +0100, Atze van der Ploeg wrote: the

...
equality relation.

Clear now or did I misunderstand?

Here is my proposed equality and ordering on the complex numbers:

data Complex = Complex (Double, Double) deriving (Eq, Ord)

Does this violate any of my requested conditions? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Roman Cheplyaka

11:37 a.m.

New subject: ordNub

The set of all values of the type is always enumerable (it's even recursive, since otherwise you wouldn't be able to tell if something is a value or not). Since it's enumerable, you can enumerate all values of that type: v1, v2, v3, ... Take x1 < x2 iff x1 precedes x2 in the above sequence. This is obviously computable. Roman On 01/01/15 17:31, Atze van der Ploeg wrote:

...

...
(That said, I don't understand why this discussion is relevant at all. The fact that the ordering exists doesn't mean that one would want to declare the Ord instance, like with complex numbers.)

It's not relevant, it's just an intellectual exercise.

For any set with a equality relation there exists a total order relation on that set consistent with the equality relation. The question is then whether there exists a set with a computable equality relation such that there is no computable total order.

I think the following computable function shows that it is always possible (it chooses an order during queries):

Maintain a table, initially emtpy

As soon as (a <= b) is requested, see if a and b are already in the table (using the computatble equality function) , if so, use their ordering in the table. If an element is not in the table, add it.

Hence the table gives a consistent total order (it depends on which ordering queries are requested, but that is not relevant?)

2015-01-01 16:06 GMT+01:00 Atze van der Ploeg mailto:atzeus@gmail.com>:

Nope you're right. Indeed uncompatible with the field structure. Now I'm confused :)

I now understand your question, but do not immediately know the answer. Anyone?

On Jan 1, 2015 4:02 PM, "Tom Ellis" mailto:tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

On Thu, Jan 01, 2015 at 03:52:26PM +0100, Atze van der Ploeg wrote: > If we do not require that (a <= b) && (a >= b) ==> a == b (where <= is > from the total ordering and == is from the equality relation) then it is > trivial, take the total ordering forall x y. x <= y that i mentioned > earlier. > > So the compatiblity with equality (you say field structure) is not besides > the point, in fact antisymmetry means that the ordering corresponds to the > equality relation. > > Clear now or did I misunderstand?

Here is my proposed equality and ordering on the complex numbers:

data Complex = Complex (Double, Double) deriving (Eq, Ord)

Does this violate any of my requested conditions? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Roman Cheplyaka

10:06 a.m.

New subject: ordNub

You misunderstood. Complex numbers can be ordered in a way that is compatible with the equality — the lexicographic ordering. (That said, I don't understand why this discussion is relevant at all. The fact that the ordering exists doesn't mean that one would want to declare the Ord instance, like with complex numbers.) On 01/01/15 16:52, Atze van der Ploeg wrote:

...

If we do not require that (a <= b) && (a >= b) ==> a == b (where <= is from the total ordering and == is from the equality relation) then it is trivial, take the total ordering forall x y. x <= y that i mentioned earlier.

So the compatiblity with equality (you say field structure) is not besides the point, in fact antisymmetry means that the ordering corresponds to the equality relation.

Clear now or did I misunderstand?

Cheers

2015-01-01 15:39 GMT+01:00 Tom Ellis mailto:tom-lists-haskell-cafe-2013@jaguarpaw.co.uk>:

On Thu, Jan 01, 2015 at 03:37:09PM +0100, Atze van der Ploeg wrote: > This boils down to the question whether on each set with an equality > relation defined on it a total ordering (consistent with the equality > relation) can also be defined.

I agree with the essence of this restatement.

> One counterexample is the complex numbers.

This is what I don't understand. The complex numbers can be totally ordered. (Not in a way compatible with the field structure, but that's beside the point).

Tom Ellis

9:18 a.m.

New subject: ordNub

On Thu, Jan 01, 2015 at 02:14:16PM +0000, Tom Ellis wrote:

...

So let me clarify that I want (<=) to be a total order in the sense that it is

* reflexive * symmetric * transitive

and `(x <= y) && (y <= x)` implies that `x == y`. (*)

Correction: I mean "antisymmetric" not "symmetric". Anti-symmetry is exactly this condition (*). Futhermore I want (==) to be at least as fine-grained as extensional equivalence. Tom

3792

Age (days ago)

3792

Last active (days ago)

List overview

Download

16 comments

4 participants

participants (4)

Atze van der Ploeg
oleg＠okmij.org
Roman Cheplyaka
Tom Ellis