Add Ord Laws to next Haskell Report
Carter Schonwald
carter.schonwald at gmail.com
Thu Feb 7 21:41:40 UTC 2019
hey Andrew B,
agreed, partial orders aren't covered by Ord, and we are discussing only
Ord here.
theres a lot of good approaches to partial ords, but thats outside of scope
for now :)
On Thu, Feb 7, 2019 at 4:37 PM Andrew Butterfield <
Andrew.Butterfield at scss.tcd.ie> wrote:
> Given that compare :: ... -> Ordering and Ordering = LT | EQ | GT,
> then the current Ord class has to support *total* orders, as there is no
> way to indicate when two elements are incomparable.
>
> Imagine trying to define the obvious partial ordering on sets - i.e.
> subset-or-equal using the Ord class.
> What should be the result, for Instance Ord (Set Int) of
>
> compare (fromList [1]) (fromList [2]) or fromList [2] <= fromList [1] ?
>
>
> Cheers, Andrew
>
> On 7 Feb 2019, at 16:21, Elliot Cameron <eacameron at gmail.com> wrote:
>
> While I'm sure it would be a lot of churn, couldn't we introduce a
> `TotalOrd` class and guard it more carefully?
>
> On Thu, Feb 7, 2019 at 10:45 AM Merijn Verstraaten <merijn at inconsistent.nl>
> wrote:
>
>> I was discussing this with Carter on IRC, so to chime in with my two
>> cents:
>>
>> I think the default behaviour for Float/Double should use a trapping NaN.
>> The current value NaN is as if every Double value has an implicit
>> "fromJust" and finding out which part of larger computations/pipelines
>> introduced the NaNs in your output is a pain.
>>
>> Trapping NaN would also eliminate the brokenness of Ord. If some people
>> are really attached to value NaNs (why?!? What's wrong with you?) we could
>> allow disabling trapping at compile or runtime so they get the old
>> behaviour.
>>
>> Cheers,
>> Merijn
>>
>> > On 7 Feb 2019, at 03:43, 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
>>
>> _______________________________________________
>> 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
>
>
> --------------------------------------------------------------------
> Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
> Lero at TCD, Head of Foundations & Methods Research Group
> School of Computer Science and Statistics,
> Room G.39, O'Reilly Institute, Trinity College, University of Dublin
> http://www.scss.tcd.ie/Andrew.Butterfield/
> --------------------------------------------------------------------
>
> _______________________________________________
> 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/20190207/5b24d0a2/attachment.html>
More information about the Libraries
mailing list