Add Ord Laws to next Haskell Report

[chessai .]

Sure. There are no explicit mention of the laws of Ord. I think they
should be explicitly stated in the report, perhaps like so:

---------- start proposed change
class  (Eq a) => Ord a  where
    compare              :: a -> a -> Ordering
    (<), (<=), (>), (>=) :: a -> a -> Bool
    max, min             :: a -> a -> a

    compare x y = if x == y then EQ
                  else if x <= y then LT
                  else GT

    x <  y = case compare x y of { LT -> True;  _ -> False }
    x <= y = case compare x y of { GT -> False; _ -> True }
    x >  y = case compare x y of { GT -> True;  _ -> False }
    x >= y = case compare x y of { LT -> False; _ -> True }

    max x y = if x <= y then y else x
    min x y = if x <= y then x else y
    {-# MINIMAL compare | (<=) #-}

The `Ord` class is used for totally ordered datatypes. Instances of
'Ord' can be derived for any user-defined datatype whose constituent
types are in 'Ord'. The declared order of the constructors in the data
declaration determines the ordering in the derived 'Ord' instances.
The 'Ordering' datatype allows a single comparison to determine the
precise ordering of two objects.

A minimal instance of 'Ord' implements either 'compare' or '<=', and
is expected to adhere to the following laws:

Antisymmetry (a <= b && b <= a = a == b)
Transitivity (a <= b && b <= c = a <= c)
Totality (a <= b || b <= a = True)

An additional law, Reflexity, is implied by Totality. It states (x <= x = True).
---------- end proposed change

I don't particularly like the bit in the current documentation about
(<=) implementing a non-strict partial ordering, because if (<=)
constitutes a minimal definition of Ord and is required only to be a
partial ordering on the type parameterised by Ord, then why is Ord
required to be a total ordering? That seems sort of confusing. It
seems to me that the current documentation leans more toward 'Ord'
implementing a partial order than a total order. I can't speak for
others, but when I think of 'Ord' I usually think of a total ordering.

Additionally, Reflexity is strictly weaker than Totality, so
specifying their relationship (Reflexivity is implied by Totality) and
also writing out what Totality means in the context of Ord makes sense
to me.

For Eq, the report currently states:

----------begin report quote
  class  Eq a  where
        (==), (/=)  ::  a -> a -> Bool

        x /= y  = not (x == y)
        x == y  = not (x /= y)

The Eq class provides equality (==) and inequality (/=) methods. All
basic datatypes except for functions and IO are instances of this
class. Instances of Eq can be derived for any user-defined datatype
whose constituents are also instances of Eq.

This declaration gives default method declarations for both /= and ==,
each being defined in terms of the other. If an instance declaration
for Eq defines neither == nor /=, then both will loop. If one is
defined, the default method for the other will make use of the one
that is defined. If both are defined, neither default method is used.
----------end report quote

I think the following changes make sense:

---------- begin proposed changes

class  Eq a  where
    (==), (/=)           :: a -> a -> Bool
    x /= y               = not (x == y)
    x == y              = not (x /= y)

The 'Eq' class defines equality ('==') and inequality ('/=').
All the basic datatypes exported by the "Prelude" are instances of 'Eq',
and 'Eq' may be derived for any datatype whose constituents are also
instances of 'Eq'.

'==' implements an equivalence relationship where two values comparing equal
are considered indistinguishable. A minimal instance of 'Eq'
implements either '==' or '/=', and must adhere to the following laws:

Reflexivity (x == x = True)
Symmetry (x == y = y == x)
Transitivity (x == y && y == z = x == z)
Substitutivity (x == y = f x == f y)
Negation (x /= y = not (x = y)
---------- end proposed changes

On Wed, Feb 6, 2019 at 3:52 PM Herbert Valerio Riedel
<hvriedel at gmail.com> wrote:
>
>
>
>
>
> On Wed, Feb 6, 2019 at 9:43 PM chessai . <chessai1996 at gmail.com> wrote:
>>
>> Per GHC.Classes (haddock-viewable from Data.Ord)
>>
>> "The Haskell Report defines no laws for Ord. However, <= is
>> customarily expected to implement a non-strict partial order and have
>> the following properties:"
>>
>> I propose that in the next report that the expected typeclass laws for
>> Ord be added. They're generally agreed upon/understood.
>
>
>
> Can you spell out the concrete change to the report wording you're suggesting? For reference, the current wording used in the 2010 Haskell Report is quoted below. While at it, you might also want to take into account the `Eq` class definition in the report.
>
>
> 6.3.2 The Ord Class
>
>   class  (Eq a) => Ord a  where
>     compare              :: a -> a -> Ordering
>     (<), (<=), (>=), (>) :: a -> a -> Bool
>     max, min             :: a -> a -> a
>
>     compare x y | x == y    = EQ
>                 | x <= y    = LT
>                 | otherwise = GT
>
>     x <= y  = compare x y /= GT
>     x <  y  = compare x y == LT
>     x >= y  = compare x y /= LT
>     x >  y  = compare x y == GT
>
>     -- Note that (min x y, max x y) = (x,y) or (y,x)
>     max x y | x <= y    =  y
>             | otherwise =  x
>     min x y | x <= y    =  x
>             | otherwise =  y
>
> The Ord class is used for totally ordered datatypes. All basic datatypes except for functions, IO, and IOError, are instances of this class. Instances of Ord can be derived for any user-defined datatype whose constituent types are in Ord. The declared order of the constructors in the data declaration determines the ordering in derived Ord instances. The Ordering datatype allows a single comparison to determine the precise ordering of two objects.
>
> The default declarations allow a user to create an Ord instance either with a type-specific compare function or with type-specific == and <= functions.
>
>
>