Add Ord Laws to next Haskell Report
Carter Schonwald
carter.schonwald at gmail.com
Thu Feb 7 03:46:43 UTC 2019
(and to be even clearer, its definitely something where any help on
determining impact and minimizing it would be a pure joy to have )
On Wed, Feb 6, 2019 at 10:42 PM Carter Schonwald <carter.schonwald at gmail.com>
wrote:
> true, i just actually WANT to fixup those corners of float, assuming
> impact can be managed suitably
>
> On Wed, Feb 6, 2019 at 10:30 PM David Feuer <david.feuer at gmail.com> wrote:
>
>> 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/2dbcb53b/attachment.html>
More information about the Libraries
mailing list