(names for) invariants for Eq and Ord?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

(names for) invariants for Eq and Ord?

Johannes Waldmann-2
Dear Cafe,

I am somewhat surprised that the Haskell Standard (*)
https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1270006.3
does not contain any
notation for (intended) properties of Eq and Ord instances,
and their relation. For Java (standard library),
the API spec uses wording like "consistent with equals"
https://docs.oracle.com/javase/10/docs/api/java/lang/Comparable.html

I am well aware that semantics (transitivity, etc.)
cannot be enforced statically, in either language.
But both standards still speak of "total order".
Do we (Haskell) need something similar to "consistent with equals"?

It depends. E.g., looking at a (random) source in containers
(Data.Map.Internal), it seems that it will always use the result of
compare, never of (==), on keys. That's not obvious from the docs.
I just checked -- I can make a type where (==) = undefined,
but write a proper Ord instance, and use it as key type.

I am asking this because I will be teaching type classes,
with Eq and Ord as examples. I detected the funny situation
that the Java specification looks "more mathematical"
than the corresponding Haskell one. What will the students think ...

- J.W.

(*) The Haskell standard is what you find when you scroll
down, down, down to the very bottom of
https://www.haskell.org/documentation . So, probably not that important...
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: (names for) invariants for Eq and Ord?

Brandon Allbery
One thing to consider is that, if you look at the Report specification for derived Ord instances and of the default (compare), you'll find that it explicitly depends on (==). So you don't actually need a "law" here.

On Tue, May 29, 2018 at 3:03 PM Johannes Waldmann <[hidden email]> wrote:
Dear Cafe,

I am somewhat surprised that the Haskell Standard (*)
https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1270006.3
does not contain any
notation for (intended) properties of Eq and Ord instances,
and their relation. For Java (standard library),
the API spec uses wording like "consistent with equals"
https://docs.oracle.com/javase/10/docs/api/java/lang/Comparable.html

I am well aware that semantics (transitivity, etc.)
cannot be enforced statically, in either language.
But both standards still speak of "total order".
Do we (Haskell) need something similar to "consistent with equals"?

It depends. E.g., looking at a (random) source in containers
(Data.Map.Internal), it seems that it will always use the result of
compare, never of (==), on keys. That's not obvious from the docs.
I just checked -- I can make a type where (==) = undefined,
but write a proper Ord instance, and use it as key type.

I am asking this because I will be teaching type classes,
with Eq and Ord as examples. I detected the funny situation
that the Java specification looks "more mathematical"
than the corresponding Haskell one. What will the students think ...

- J.W.

(*) The Haskell standard is what you find when you scroll
down, down, down to the very bottom of
https://www.haskell.org/documentation . So, probably not that important...
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: (names for) invariants for Eq and Ord?

Haskell - Haskell-Cafe mailing list
In reply to this post by Johannes Waldmann-2
Hi Johannes,


Cheers,
Simon

2018-05-28 16:47 GMT+02:00 Johannes Waldmann <[hidden email]>:
Dear Cafe,

I am somewhat surprised that the Haskell Standard (*)
https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1270006.3
does not contain any
notation for (intended) properties of Eq and Ord instances,
and their relation. For Java (standard library),
the API spec uses wording like "consistent with equals"
https://docs.oracle.com/javase/10/docs/api/java/lang/Comparable.html

I am well aware that semantics (transitivity, etc.)
cannot be enforced statically, in either language.
But both standards still speak of "total order".
Do we (Haskell) need something similar to "consistent with equals"?

It depends. E.g., looking at a (random) source in containers
(Data.Map.Internal), it seems that it will always use the result of
compare, never of (==), on keys. That's not obvious from the docs.
I just checked -- I can make a type where (==) = undefined,
but write a proper Ord instance, and use it as key type.

I am asking this because I will be teaching type classes,
with Eq and Ord as examples. I detected the funny situation
that the Java specification looks "more mathematical"
than the corresponding Haskell one. What will the students think ...

- J.W.

(*) The Haskell standard is what you find when you scroll
down, down, down to the very bottom of
https://www.haskell.org/documentation . So, probably not that important...
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: (names for) invariants for Eq and Ord?

Levent Erkok
Johannes:

Heartily agreed. In fact, oft-used modules like Data.Map also need to be very clear regarding their requirements for Eq/Ord. It's well known in the folklore that the law:

          M.lookup k (M.insert k v M.empty) == Just v

fails for maps when the key can be floating point:

    Prelude> import qualified Data.Map as M
    Prelude M> let k = 0/0 in let v = 0 in M.lookup k (M.insert k v M.empty) == Just v
    False

Perhaps not a big deal as no-one should use floating-point values as a key to a map, but there's nothing stopping from anyone from doing so. Perhaps more worryingly, the Haskell report is largely silent about  Eq/Ord instances that come out-of-the-box for such gotchas as you yourself observed.

-Levent.


On Tue, May 29, 2018 at 12:26 PM, Simon Jakobi via Haskell-Cafe <[hidden email]> wrote:
Hi Johannes,


Cheers,
Simon

2018-05-28 16:47 GMT+02:00 Johannes Waldmann <[hidden email]>:
Dear Cafe,

I am somewhat surprised that the Haskell Standard (*)
https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1270006.3
does not contain any
notation for (intended) properties of Eq and Ord instances,
and their relation. For Java (standard library),
the API spec uses wording like "consistent with equals"
https://docs.oracle.com/javase/10/docs/api/java/lang/Comparable.html

I am well aware that semantics (transitivity, etc.)
cannot be enforced statically, in either language.
But both standards still speak of "total order".
Do we (Haskell) need something similar to "consistent with equals"?

It depends. E.g., looking at a (random) source in containers
(Data.Map.Internal), it seems that it will always use the result of
compare, never of (==), on keys. That's not obvious from the docs.
I just checked -- I can make a type where (==) = undefined,
but write a proper Ord instance, and use it as key type.

I am asking this because I will be teaching type classes,
with Eq and Ord as examples. I detected the funny situation
that the Java specification looks "more mathematical"
than the corresponding Haskell one. What will the students think ...

- J.W.

(*) The Haskell standard is what you find when you scroll
down, down, down to the very bottom of
https://www.haskell.org/documentation . So, probably not that important...
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: (names for) invariants for Eq and Ord?

David Feuer
I won't even commit to making sure Map operations are *deterministic* in the face of a non-reflexive ==.

On Tue, May 29, 2018, 4:01 PM Levent Erkok <[hidden email]> wrote:
Johannes:

Heartily agreed. In fact, oft-used modules like Data.Map also need to be very clear regarding their requirements for Eq/Ord. It's well known in the folklore that the law:

          M.lookup k (M.insert k v M.empty) == Just v

fails for maps when the key can be floating point:

    Prelude> import qualified Data.Map as M
    Prelude M> let k = 0/0 in let v = 0 in M.lookup k (M.insert k v M.empty) == Just v
    False

Perhaps not a big deal as no-one should use floating-point values as a key to a map, but there's nothing stopping from anyone from doing so. Perhaps more worryingly, the Haskell report is largely silent about  Eq/Ord instances that come out-of-the-box for such gotchas as you yourself observed.

-Levent.


On Tue, May 29, 2018 at 12:26 PM, Simon Jakobi via Haskell-Cafe <[hidden email]> wrote:
Hi Johannes,


Cheers,
Simon

2018-05-28 16:47 GMT+02:00 Johannes Waldmann <[hidden email]>:
Dear Cafe,

I am somewhat surprised that the Haskell Standard (*)
https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1270006.3
does not contain any
notation for (intended) properties of Eq and Ord instances,
and their relation. For Java (standard library),
the API spec uses wording like "consistent with equals"
https://docs.oracle.com/javase/10/docs/api/java/lang/Comparable.html

I am well aware that semantics (transitivity, etc.)
cannot be enforced statically, in either language.
But both standards still speak of "total order".
Do we (Haskell) need something similar to "consistent with equals"?

It depends. E.g., looking at a (random) source in containers
(Data.Map.Internal), it seems that it will always use the result of
compare, never of (==), on keys. That's not obvious from the docs.
I just checked -- I can make a type where (==) = undefined,
but write a proper Ord instance, and use it as key type.

I am asking this because I will be teaching type classes,
with Eq and Ord as examples. I detected the funny situation
that the Java specification looks "more mathematical"
than the corresponding Haskell one. What will the students think ...

- J.W.

(*) The Haskell standard is what you find when you scroll
down, down, down to the very bottom of
https://www.haskell.org/documentation . So, probably not that important...
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: (names for) invariants for Eq and Ord?

Olaf Klinke
In reply to this post by Johannes Waldmann-2
Prelude> import qualified Data.Map as M
   Prelude M> let k = 0/0 in let v = 0 in M.lookup k (M.insert k v
M.empty) == Just v
   False

This one is not surprising because the presence of 0/0 destroys the total order of Double, so strictly speaking this should not have an Ord instance.

Olaf
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: (names for) invariants for Eq and Ord?

Joachim Breitner-2
In reply to this post by Johannes Waldmann-2
Hi Johannes,

Am Montag, den 28.05.2018, 16:47 +0200 schrieb Johannes Waldmann:
> Do we (Haskell) need something similar to "consistent with equals"?

not authorative, but the formalization of the base library in Coq, as
part of the the hs-to-coq project, says Eq and Ord need to be
compatible:

Class OrdLaws (t : Type) {HEq : Eq_ t} {HOrd : Ord t} {HEqLaw : EqLaws t} :=
  { (* The axioms *)
    Ord_antisym  : forall a b, a <= b = true -> b <= a = true -> a == b = true;
    Ord_trans_le : forall a b c, a <= b = true -> b <= c = true -> a <= c = true;
    Ord_total    : forall a b, a <= b = true \/ b <= a = true;
    (* The other operations, in terms of <= or == *)
    Ord_compare_Lt : forall a b, compare a b = Lt <-> b <= a = false;
    Ord_compare_Eq : forall a b, compare a b = Eq <-> a == b = true;
    Ord_compare_Gt : forall a b, compare a b = Gt <-> a <= b = false;
    Ord_lt_le : forall a b, a < b = negb (b <= a);
    Ord_ge_le : forall a b, a >= b = (b <= a);
    Ord_gt_le : forall a b, a >  b = negb (a <= b);
}.

https://github.com/antalsz/hs-to-coq/blob/86f4c36dfe4b096eb7d48205cea3fddeeab23eaa/examples/containers/theories/OrdTactic.v#L14

Because we have a tactic that automates reasoning with lawfull Ord
instances and uses Ord_antisym and Ord_compare_Eq internally I cannot
easily check if these laws are actually used in the verification of
Data.Set.

One could argue that “total order” implies “antisymmetric” which
implies a relation with (==).

Cheers,
Joachim
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (849 bytes) Download Attachment