Add Ord Laws to next Haskell Report
David Feuer
david.feuer at gmail.com
Thu Feb 7 03:30:00 UTC 2019
We can add laws while recognizing that some existing instances are not
lawful.
On Wed, Feb 6, 2019, 9:43 PM Carter Schonwald <carter.schonwald at gmail.com
wrote:
> We cant add laws at the moment unless we change how the Ord instances for
> Float and Double are defined. (which i think SHOULd happen, but needs some
> care and has lots of implications)
>
> there are several possible semantics we can choose that act as we expect
> on +/- infity and finite floats, but differ in the handling of nans
>
> option 1) use the total order defined in floating point standard 2008,
> section 5.10, which defines negative nans below -infity, positive nans
> above +infty
> (this has the nice property that you could check for not nan by -infty
> <= x && x <= infty)
>
> option 2) shift haskell/ GHC to having signalling NAN semantics by
> default, so the only "fully evaluated" floating point values are in the
> interval from negative to positive infinity ,
>
> option 3) some mixture of the above
>
> I am slowly doing some patches to improve floating point bits in ghc (and
> pave the way towards doing something like one of the above), though theres
> still much to do
>
> also: the current definitions of min/max via compare aren't commutative if
> either argument is nan (they become right biased or left biased, i forget
> which)
>
> http://www.dsc.ufcg.edu.br/~cnum/modulos/Modulo2/IEEE754_2008.pdf is a
> copy of ieee floating point 2008 (easy to google up a copy if that link
> doesnt work)
>
>
>
>
> On Wed, Feb 6, 2019 at 4:31 PM chessai . <chessai1996 at gmail.com> wrote:
>
>> 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.
>> >
>> >
>> >
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20190206/5b13b137/attachment-0001.html>
More information about the Libraries
mailing list