Add Ord Laws to next Haskell Report

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
47 messages Options
123
Reply | Threaded
Open this post in threaded view
|

Add Ord Laws to next Haskell Report

chessai .
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.
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Herbert Valerio Riedel-3




On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Tikhon Jelvis
Does the wording of the report specify "totally ordered" as a law? I think it would be good to make that explicit, laying out the axioms for what a total order is—similar to the current documentation in Data.Ord but explicitly as the laws for the class.

The relationship between Eq and Ord should be explicitly specified too, if it isn't.

On Wed, Feb 6, 2019, 12:53 Herbert Valerio Riedel <[hidden email] wrote:




On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

chessai .
In reply to this post by Herbert Valerio Riedel-3
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
<[hidden email]> wrote:

>
>
>
>
>
> On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Carter Schonwald
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 . <[hidden email]> 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
<[hidden email]> wrote:
>
>
>
>
>
> On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

David Feuer
We can add laws while recognizing that some existing instances are not lawful.

On Wed, Feb 6, 2019, 9:43 PM Carter Schonwald <[hidden email] 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 . <[hidden email]> 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
<[hidden email]> wrote:
>
>
>
>
>
> On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Carter Schonwald
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 <[hidden email]> wrote:
We can add laws while recognizing that some existing instances are not lawful.

On Wed, Feb 6, 2019, 9:43 PM Carter Schonwald <[hidden email] 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 . <[hidden email]> 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
<[hidden email]> wrote:
>
>
>
>
>
> On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Carter Schonwald
(and to be even clearer, its definitely something where any help on determining impact and minimizing it would be a pure joy to have )

On Wed, Feb 6, 2019 at 10:42 PM Carter Schonwald <[hidden email]> wrote:
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 <[hidden email]> wrote:
We can add laws while recognizing that some existing instances are not lawful.

On Wed, Feb 6, 2019, 9:43 PM Carter Schonwald <[hidden email] 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 . <[hidden email]> 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
<[hidden email]> wrote:
>
>
>
>
>
> On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Carter Schonwald
I guess the OTHER important reason is: any code that assumes those putative laws will break horribly on floating point data types in the presence of NAN values for any code that assumes those laws  (but only when NANs happen )

On Wed, Feb 6, 2019 at 10:46 PM Carter Schonwald <[hidden email]> wrote:
(and to be even clearer, its definitely something where any help on determining impact and minimizing it would be a pure joy to have )

On Wed, Feb 6, 2019 at 10:42 PM Carter Schonwald <[hidden email]> wrote:
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 <[hidden email]> wrote:
We can add laws while recognizing that some existing instances are not lawful.

On Wed, Feb 6, 2019, 9:43 PM Carter Schonwald <[hidden email] 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 . <[hidden email]> 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
<[hidden email]> wrote:
>
>
>
>
>
> On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

chessai .
Yeah, Float/Double are always a problem when it comes to Ord. I think
it might be best to just acknowledge their unlawfulness.  It's
unfortunate that they have Ord instances at all, IMO, but at this
point there's no changing that.

On Thu, Feb 7, 2019 at 12:02 AM Carter Schonwald
<[hidden email]> wrote:

>
> I guess the OTHER important reason is: any code that assumes those putative laws will break horribly on floating point data types in the presence of NAN values for any code that assumes those laws  (but only when NANs happen )
>
> On Wed, Feb 6, 2019 at 10:46 PM Carter Schonwald <[hidden email]> wrote:
>>
>> (and to be even clearer, its definitely something where any help on determining impact and minimizing it would be a pure joy to have )
>>
>> On Wed, Feb 6, 2019 at 10:42 PM Carter Schonwald <[hidden email]> wrote:
>>>
>>> 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 <[hidden email]> wrote:
>>>>
>>>> We can add laws while recognizing that some existing instances are not lawful.
>>>>
>>>> On Wed, Feb 6, 2019, 9:43 PM Carter Schonwald <[hidden email] 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 . <[hidden email]> 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
>>>>>> <[hidden email]> wrote:
>>>>>> >
>>>>>> >
>>>>>> >
>>>>>> >
>>>>>> >
>>>>>> > On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
>>>>>> [hidden email]
>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>
>>>>> _______________________________________________
>>>>> Libraries mailing list
>>>>> [hidden email]
>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Merijn Verstraaten
In reply to this post by Carter Schonwald
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 <[hidden email]> 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 . <[hidden email]> 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
> <[hidden email]> wrote:
> >
> >
> >
> >
> >
> > On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Elliot Cameron-2
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 <[hidden email]> 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 <[hidden email]> 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 . <[hidden email]> 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
> <[hidden email]> wrote:
> >
> >
> >
> >
> >
> > On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Henning Thielemann
In reply to this post by Merijn Verstraaten

On Thu, 7 Feb 2019, Merijn Verstraaten wrote:

> 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"

I like to think of it like all operations are lifted to (Maybe Float).

> 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.

What about calling into foreign code? If I call a BLAS routine and one
element of the result vector is NaN, shall this be trapped? Or shall it be
trapped once I access the NaN element?
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Andrew Butterfield-2
In reply to this post by Elliot Cameron-2
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 . <[hidden email]> 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
> <[hidden email]> wrote:
> >
> >
> >
> >
> >
> > On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Sven Panne-2
In reply to this post by Henning Thielemann
Am Do., 7. Feb. 2019 um 17:22 Uhr schrieb Henning Thielemann <[hidden email]>:
[...] What about calling into foreign code? If I call a BLAS routine and one
element of the result vector is NaN, shall this be trapped? Or shall it be
trapped once I access the NaN element?

IMHO this is the biggest show stopper for some exotic NaN handling, as correct as it may be mathematically or aesthetically: The floating point environment is a thread-local (i.e. basically global) entity on most platforms, and most programming language runtimes expect a "default" environment, i.e. no traps when NaNs are encountered. So if Haskell wants to do things differently, the FPE has to be set/reset around foreign calls and for around every Haskell callback. I am not sure if this is really worth the trouble and the performance loss. For some special applications it might be OK or even important, but my gut feeling is that trapping NaNs is the wrong default in our current world...

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Carter Schonwald
@sven and @henning : 
i'm actually doing some preliminary work to add save and restore for FPU state to the GHC RTS, at the green/haskell thread layer. after first ripping out x87 code gen, which just needs some more docs written out before its merged in. note that i'm speaking specifically of the MXCSR register save and restore, not the more hefty operations you might be thinking.

FPU mode state save and restore is done already on EVERY OS when switching threads/processes, and in the agner fog latency tables  the cost of manipulating  mxcsr registers is pretty small!

LDMXCSR  (restore) and STMXCSR  (save) have cpu latencies at like 5-20 cycles  (more often 8-15), so having the current C ffi calls set the default C FPU environment (as we currently have ordinarily) is super doable to ensure no breakage of existing C bindings, plus have a new ccall variant that inherits the host haskell thread FPU state.  we're talking sub 10 nanosecond overhead on x86 and x86_64 platforms (and either way, on those platforms soon ghc will only be using the sse2 or higher ).

point being: aside from like AMD piledriver micro architecture and some stuff from VIA, the performance of the CPU instruction for the signalling nans state setup and related rounding mode etc, should work perfectly well, 

[hidden email]  I do not support documenting false laws in any enshrined way, it will result in broken code. (Also i'm actually working to do some fixes, if you reread my remarks and merijn's, and i think we can have our cake and eat it, with the finest floats). Lets fix stuff and then document true laws!



On Thu, Feb 7, 2019 at 12:05 PM Sven Panne <[hidden email]> wrote:
Am Do., 7. Feb. 2019 um 17:22 Uhr schrieb Henning Thielemann <[hidden email]>:
[...] What about calling into foreign code? If I call a BLAS routine and one
element of the result vector is NaN, shall this be trapped? Or shall it be
trapped once I access the NaN element?

IMHO this is the biggest show stopper for some exotic NaN handling, as correct as it may be mathematically or aesthetically: The floating point environment is a thread-local (i.e. basically global) entity on most platforms, and most programming language runtimes expect a "default" environment, i.e. no traps when NaNs are encountered. So if Haskell wants to do things differently, the FPE has to be set/reset around foreign calls and for around every Haskell callback. I am not sure if this is really worth the trouble and the performance loss. For some special applications it might be OK or even important, but my gut feeling is that trapping NaNs is the wrong default in our current world...
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Carter Schonwald
to further add weight, i'm still doing preliminary hackery on the signalling approach, but the signalling for FP state stuff seems to be OS thread local, so it can be treated as an exception perfectly well!

On Thu, Feb 7, 2019 at 4:27 PM Carter Schonwald <[hidden email]> wrote:
@sven and @henning : 
i'm actually doing some preliminary work to add save and restore for FPU state to the GHC RTS, at the green/haskell thread layer. after first ripping out x87 code gen, which just needs some more docs written out before its merged in. note that i'm speaking specifically of the MXCSR register save and restore, not the more hefty operations you might be thinking.

FPU mode state save and restore is done already on EVERY OS when switching threads/processes, and in the agner fog latency tables  the cost of manipulating  mxcsr registers is pretty small!

LDMXCSR  (restore) and STMXCSR  (save) have cpu latencies at like 5-20 cycles  (more often 8-15), so having the current C ffi calls set the default C FPU environment (as we currently have ordinarily) is super doable to ensure no breakage of existing C bindings, plus have a new ccall variant that inherits the host haskell thread FPU state.  we're talking sub 10 nanosecond overhead on x86 and x86_64 platforms (and either way, on those platforms soon ghc will only be using the sse2 or higher ).

point being: aside from like AMD piledriver micro architecture and some stuff from VIA, the performance of the CPU instruction for the signalling nans state setup and related rounding mode etc, should work perfectly well, 

[hidden email]  I do not support documenting false laws in any enshrined way, it will result in broken code. (Also i'm actually working to do some fixes, if you reread my remarks and merijn's, and i think we can have our cake and eat it, with the finest floats). Lets fix stuff and then document true laws!



On Thu, Feb 7, 2019 at 12:05 PM Sven Panne <[hidden email]> wrote:
Am Do., 7. Feb. 2019 um 17:22 Uhr schrieb Henning Thielemann <[hidden email]>:
[...] What about calling into foreign code? If I call a BLAS routine and one
element of the result vector is NaN, shall this be trapped? Or shall it be
trapped once I access the NaN element?

IMHO this is the biggest show stopper for some exotic NaN handling, as correct as it may be mathematically or aesthetically: The floating point environment is a thread-local (i.e. basically global) entity on most platforms, and most programming language runtimes expect a "default" environment, i.e. no traps when NaNs are encountered. So if Haskell wants to do things differently, the FPE has to be set/reset around foreign calls and for around every Haskell callback. I am not sure if this is really worth the trouble and the performance loss. For some special applications it might be OK or even important, but my gut feeling is that trapping NaNs is the wrong default in our current world...
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

David Feuer
Even if Ord becomes lawful for floating point, there will still be massive problems reasoning about it because the Num instances can't support the ring laws, let alone the ordered ring laws. What should `compare NaN n` be? If it's an exception, then the ordering is not total, you can't store NaN in a Set, etc. If it's LT or GT, then you get a total ordering, but a rather weird one. So yeah, you'd be able to store NaN in a Set and have an NaN key in a Map, but then as soon as you start looking at where these are coming from and where they're going, everything goes weird and you need type-specific code anyway.

On Thu, Feb 7, 2019, 4:29 PM Carter Schonwald <[hidden email] wrote:
to further add weight, i'm still doing preliminary hackery on the signalling approach, but the signalling for FP state stuff seems to be OS thread local, so it can be treated as an exception perfectly well!

On Thu, Feb 7, 2019 at 4:27 PM Carter Schonwald <[hidden email]> wrote:
@sven and @henning : 
i'm actually doing some preliminary work to add save and restore for FPU state to the GHC RTS, at the green/haskell thread layer. after first ripping out x87 code gen, which just needs some more docs written out before its merged in. note that i'm speaking specifically of the MXCSR register save and restore, not the more hefty operations you might be thinking.

FPU mode state save and restore is done already on EVERY OS when switching threads/processes, and in the agner fog latency tables  the cost of manipulating  mxcsr registers is pretty small!

LDMXCSR  (restore) and STMXCSR  (save) have cpu latencies at like 5-20 cycles  (more often 8-15), so having the current C ffi calls set the default C FPU environment (as we currently have ordinarily) is super doable to ensure no breakage of existing C bindings, plus have a new ccall variant that inherits the host haskell thread FPU state.  we're talking sub 10 nanosecond overhead on x86 and x86_64 platforms (and either way, on those platforms soon ghc will only be using the sse2 or higher ).

point being: aside from like AMD piledriver micro architecture and some stuff from VIA, the performance of the CPU instruction for the signalling nans state setup and related rounding mode etc, should work perfectly well, 

[hidden email]  I do not support documenting false laws in any enshrined way, it will result in broken code. (Also i'm actually working to do some fixes, if you reread my remarks and merijn's, and i think we can have our cake and eat it, with the finest floats). Lets fix stuff and then document true laws!



On Thu, Feb 7, 2019 at 12:05 PM Sven Panne <[hidden email]> wrote:
Am Do., 7. Feb. 2019 um 17:22 Uhr schrieb Henning Thielemann <[hidden email]>:
[...] What about calling into foreign code? If I call a BLAS routine and one
element of the result vector is NaN, shall this be trapped? Or shall it be
trapped once I access the NaN element?

IMHO this is the biggest show stopper for some exotic NaN handling, as correct as it may be mathematically or aesthetically: The floating point environment is a thread-local (i.e. basically global) entity on most platforms, and most programming language runtimes expect a "default" environment, i.e. no traps when NaNs are encountered. So if Haskell wants to do things differently, the FPE has to be set/reset around foreign calls and for around every Haskell callback. I am not sure if this is really worth the trouble and the performance loss. For some special applications it might be OK or even important, but my gut feeling is that trapping NaNs is the wrong default in our current world...
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Carter Schonwald
In reply to this post by Andrew Butterfield-2
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 . <[hidden email]> 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
> <[hidden email]> wrote:
> >
> >
> >
> >
> >
> > On Wed, Feb 6, 2019 at 9:43 PM chessai . <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add Ord Laws to next Haskell Report

Carter Schonwald
In reply to this post by David Feuer
David, 
We aren't talking about Ring laws here, so lets not pull that in yet please :) 

as Merijn also noted, one possible semantics is have signalling Nans, so that any haskell calculation that yields a Nan instead triggers an exception via cpu stuff. Or the next FP instruction that touches the nan will trigger in the case of it coming from C land (I just reread all the relevant sections of the intel architecture manual, its quite explicit on this corner, and still be superbly IEEE float compliant, AND place nice with code that DOES want nan via stateful stuff if need be)

on the matter of Nan, in a quiet nan universe, theres a whole universe of Nans, and they're all different, and in fact the iEEE standard is quite clear that a language could pick different nans for different errors (eg have all the bits form a bit set of possible errors). Or one of several  other approaches.

point being, we can have nice things.

mind you, i'm still doing this hackery over time. But I genuinely see a path thats thread safe, makes the MXCSR register state act local per haskell thread, doesn't change the default semantics for C ffi calls, and still allows those who want quiet NANs to do whatever they want if they really really want to. 

I do agree that any such changes can't break code in the wild that depends on FPU state stuff, nor those who like Quiet Nans more than exceptional/signalling ones. And thats a burden on me / any collaborators for successful execution.

punchline Lawful Ord and NanFree Float for all, with no leaky breakages,  Every Num has Div By Zero error already,  lets recognize all NAN computations as being similarly exceptional by default. :) 

On Thu, Feb 7, 2019 at 4:41 PM David Feuer <[hidden email]> wrote:
Even if Ord becomes lawful for floating point, there will still be massive problems reasoning about it because the Num instances can't support the ring laws, let alone the ordered ring laws. What should `compare NaN n` be? If it's an exception, then the ordering is not total, you can't store NaN in a Set, etc. If it's LT or GT, then you get a total ordering, but a rather weird one. So yeah, you'd be able to store NaN in a Set and have an NaN key in a Map, but then as soon as you start looking at where these are coming from and where they're going, everything goes weird and you need type-specific code anyway.

On Thu, Feb 7, 2019, 4:29 PM Carter Schonwald <[hidden email] wrote:
to further add weight, i'm still doing preliminary hackery on the signalling approach, but the signalling for FP state stuff seems to be OS thread local, so it can be treated as an exception perfectly well!

On Thu, Feb 7, 2019 at 4:27 PM Carter Schonwald <[hidden email]> wrote:
@sven and @henning : 
i'm actually doing some preliminary work to add save and restore for FPU state to the GHC RTS, at the green/haskell thread layer. after first ripping out x87 code gen, which just needs some more docs written out before its merged in. note that i'm speaking specifically of the MXCSR register save and restore, not the more hefty operations you might be thinking.

FPU mode state save and restore is done already on EVERY OS when switching threads/processes, and in the agner fog latency tables  the cost of manipulating  mxcsr registers is pretty small!

LDMXCSR  (restore) and STMXCSR  (save) have cpu latencies at like 5-20 cycles  (more often 8-15), so having the current C ffi calls set the default C FPU environment (as we currently have ordinarily) is super doable to ensure no breakage of existing C bindings, plus have a new ccall variant that inherits the host haskell thread FPU state.  we're talking sub 10 nanosecond overhead on x86 and x86_64 platforms (and either way, on those platforms soon ghc will only be using the sse2 or higher ).

point being: aside from like AMD piledriver micro architecture and some stuff from VIA, the performance of the CPU instruction for the signalling nans state setup and related rounding mode etc, should work perfectly well, 

[hidden email]  I do not support documenting false laws in any enshrined way, it will result in broken code. (Also i'm actually working to do some fixes, if you reread my remarks and merijn's, and i think we can have our cake and eat it, with the finest floats). Lets fix stuff and then document true laws!



On Thu, Feb 7, 2019 at 12:05 PM Sven Panne <[hidden email]> wrote:
Am Do., 7. Feb. 2019 um 17:22 Uhr schrieb Henning Thielemann <[hidden email]>:
[...] What about calling into foreign code? If I call a BLAS routine and one
element of the result vector is NaN, shall this be trapped? Or shall it be
trapped once I access the NaN element?

IMHO this is the biggest show stopper for some exotic NaN handling, as correct as it may be mathematically or aesthetically: The floating point environment is a thread-local (i.e. basically global) entity on most platforms, and most programming language runtimes expect a "default" environment, i.e. no traps when NaNs are encountered. So if Haskell wants to do things differently, the FPE has to be set/reset around foreign calls and for around every Haskell callback. I am not sure if this is really worth the trouble and the performance loss. For some special applications it might be OK or even important, but my gut feeling is that trapping NaNs is the wrong default in our current world...
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
123