Add Ord Laws to next Haskell Report
Elliot Cameron
eacameron at gmail.com
Thu Feb 7 16:21:11 UTC 2019
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20190207/f6c07353/attachment.html>
More information about the Libraries
mailing list