Add Ord Laws to next Haskell Report
Carter Schonwald
carter.schonwald at gmail.com
Thu Feb 7 03:42:29 UTC 2019
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/33b323b9/attachment.html>
More information about the Libraries
mailing list