Add Ord Laws to next Haskell Report
Andrew Butterfield
Andrew.Butterfield at scss.tcd.ie
Thu Feb 7 16:48:49 UTC 2019
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 <mailto: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 <mailto: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 <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 <mailto: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 <mailto:hvriedel at gmail.com>> wrote:
> > >
> > >
> > >
> > >
> > >
> > > On Wed, Feb 6, 2019 at 9:43 PM chessai . <chessai1996 at gmail.com <mailto: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 <mailto:Libraries at haskell.org>
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
> > _______________________________________________
> > Libraries mailing list
> > Libraries at haskell.org <mailto:Libraries at haskell.org>
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <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/
--------------------------------------------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20190207/3e8306fc/attachment.html>
More information about the Libraries
mailing list