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 < johannes.waldmann@htwk-leipzig.de> wrote:

Dear Cafe,

I am somewhat surprised that the Haskell Standard (*)

https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1270006... 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 allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

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/86f4c36dfe4b096eb7d48205cea3fddeea... 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 mail@joachim-breitner.de http://www.joachim-breitner.de/