Add Ord Laws to next Haskell Report
Carter Schonwald
carter.schonwald at gmail.com
Thu Feb 7 02:43:23 UTC 2019
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20190206/b813b444/attachment.html>
More information about the Libraries
mailing list