Ord methods too strict?

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

Ord methods too strict?

V.Liepelt
I am surprised to find that `False <= undefined = undefined`.

What justifies (<=) to be strict in both arguments?

Vilem
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Isaac Elliott
One of the relationships implied by the Ord typeclass is:

a <= b = True  iff  compare a b = EQ \/ compare a b = LT

If we write an alternative definition of (<=) that is only strict in its first argument:

False <= _ = True
True <= x = x

Then it's impossible to write `compare` in a way that's consistent with that relation.

More concretely, it's likely that Ord Bool is defined via `compare`, which is necessarily strict in both arguments.

On Wed, 2 Jan. 2019, 7:47 pm V.Liepelt, <[hidden email]> wrote:
I am surprised to find that `False <= undefined = undefined`.

What justifies (<=) to be strict in both arguments?

Vilem
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

V.Liepelt
More concretely, it's likely that Ord Bool is defined via `compare`, which is necessarily strict in both arguments.

Yes, this did come to mind. In general a non-strict `compare` would only make sense for `()`.

One of the relationships implied by the Ord typeclass is:

a <= b = True  iff  compare a b = EQ \/ compare a b = LT

So wouldn’t it make sense to define `compare` in terms of the “weaker” relations? It seems very unhaskelly to do the unnecessary work of evaluating the second argument to a relation when we already know what the result should be.

Vilem

On 2 Jan 2019, at 10:29, Isaac Elliott <[hidden email]> wrote:

One of the relationships implied by the Ord typeclass is:

a <= b = True  iff  compare a b = EQ \/ compare a b = LT

If we write an alternative definition of (<=) that is only strict in its first argument:

False <= _ = True
True <= x = x

Then it's impossible to write `compare` in a way that's consistent with that relation.

More concretely, it's likely that Ord Bool is defined via `compare`, which is necessarily strict in both arguments.

On Wed, 2 Jan. 2019, 7:47 pm V.Liepelt, <[hidden email]> wrote:
I am surprised to find that `False <= undefined = undefined`.

What justifies (<=) to be strict in both arguments?

Vilem
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Tom Ellis-5
In reply to this post by V.Liepelt
On Wed, Jan 02, 2019 at 09:47:15AM +0000, V.Liepelt wrote:
> I am surprised to find that `False <= undefined = undefined`.
>
> What justifies (<=) to be strict in both arguments?

The implementation of the Ord instance for Bool is derived, as you can see
here:

    https://www.stackage.org/haddock/lts-12.1/ghc-prim-0.5.2.0/src/GHC-Classes.html#Ord

As for the justification, perhaps it's too much of a special case for only
one value of an enumeration to compare to undefined without crashing, and
perhaps it inhibits optimisation opportunities.

Tom
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

V.Liepelt
> The implementation of the Ord instance for Bool is derived

So my argument would be—doesn’t this mean that we need to do cleverer deriving or at least have a hand-written instance?

> As for the justification, perhaps it's too much of a special case for only
> one value of an enumeration to compare to undefined without crashing

This is not just about crashing. (I’m using `undefined` as a way of making strictness explicit.) `False >= veryExpensiveComputation` should return `True` immediately without any unnecessary computation.

Also it doesn’t seem like a special case: this makes sense for any partially ordered Type with a top and/or bottom element.

> perhaps it inhibits optimisation opportunities.

That doesn’t seem very likely to me, I would rather think the contrary (see above): doing unnecessary work can hardly make a program run faster.

V

> On 2 Jan 2019, at 11:37, Tom Ellis <[hidden email]> wrote:
>
> On Wed, Jan 02, 2019 at 09:47:15AM +0000, V.Liepelt wrote:
>> I am surprised to find that `False <= undefined = undefined`.
>>
>> What justifies (<=) to be strict in both arguments?
>
> The implementation of the Ord instance for Bool is derived, as you can see
> here:
>
>    https://www.stackage.org/haddock/lts-12.1/ghc-prim-0.5.2.0/src/GHC-Classes.html#Ord
>
> As for the justification, perhaps it's too much of a special case for only
> one value of an enumeration to compare to undefined without crashing, and
> perhaps it inhibits optimisation opportunities.
>
> Tom
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Clinton Mead
How would you define Ord on Bools? Like so?

False <= _ = True
_ <= y = y

Note that even with this definition, "undefined <= True = undefined" so strictness is now not symmetric. 

Also, as bool are implemented as just an int of some sort (presumably 0 and 1), the strict definition allows the following implementation in effect:

x <= y = fromEnum x <= fromEnum y

Note "fromEnum" here is zero cost, and there is no branch. Checking the left hand branch for false first would require a branch that would possibly hit performance. This probably isn't worth slowing down this function just so it's lazy in it's right argument (but as a gotcha now, still strict in it's left argument).

On Wed, Jan 2, 2019 at 10:50 PM V.Liepelt <[hidden email]> wrote:
> The implementation of the Ord instance for Bool is derived

So my argument would be—doesn’t this mean that we need to do cleverer deriving or at least have a hand-written instance?

> As for the justification, perhaps it's too much of a special case for only
> one value of an enumeration to compare to undefined without crashing

This is not just about crashing. (I’m using `undefined` as a way of making strictness explicit.) `False >= veryExpensiveComputation` should return `True` immediately without any unnecessary computation.

Also it doesn’t seem like a special case: this makes sense for any partially ordered Type with a top and/or bottom element.

> perhaps it inhibits optimisation opportunities.

That doesn’t seem very likely to me, I would rather think the contrary (see above): doing unnecessary work can hardly make a program run faster.

V

> On 2 Jan 2019, at 11:37, Tom Ellis <[hidden email]> wrote:
>
> On Wed, Jan 02, 2019 at 09:47:15AM +0000, V.Liepelt wrote:
>> I am surprised to find that `False <= undefined = undefined`.
>>
>> What justifies (<=) to be strict in both arguments?
>
> The implementation of the Ord instance for Bool is derived, as you can see
> here:
>
>    https://www.stackage.org/haddock/lts-12.1/ghc-prim-0.5.2.0/src/GHC-Classes.html#Ord
>
> As for the justification, perhaps it's too much of a special case for only
> one value of an enumeration to compare to undefined without crashing, and
> perhaps it inhibits optimisation opportunities.
>
> Tom
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

V.Liepelt
False <= _ = True
_ <= y = y

Yeah, that’s what I was thinking (in fact this is how I hit this in the first place—I was using `(<=)` as a quick and dirty logical implication operator and was surprised to hit `undefined` even though the precondition was False!)

Note that even with this definition, "undefined <= True = undefined" so strictness is now not symmetric. 

Isn’t “asymmetry” the whole point of laziness? Consider `(||)`.

Note "fromEnum" here is zero cost, and there is no branch. Checking the left hand branch for false first would require a branch that would possibly hit performance. This probably isn't worth slowing down this function just so it's lazy in it's right argument (but as a gotcha now, still strict in it's left argument).

Yes, comparison on constants may happen to be faster on a concrete architecture. Thanks, I hadn’t considered this. However this assumes that both arguments are already evaluated, which of course will require branching unless you happen to know the second argument at compile time, for which case we might want to have a rewrite rule for the more efficient implementation. But it feels wrong to make architectural considerations leak into the standard library when this isn’t really necessary.

V

On 2 Jan 2019, at 12:09, Clinton Mead <[hidden email]> wrote:

How would you define Ord on Bools? Like so?

False <= _ = True
_ <= y = y

Note that even with this definition, "undefined <= True = undefined" so strictness is now not symmetric. 

Also, as bool are implemented as just an int of some sort (presumably 0 and 1), the strict definition allows the following implementation in effect:

x <= y = fromEnum x <= fromEnum y

Note "fromEnum" here is zero cost, and there is no branch. Checking the left hand branch for false first would require a branch that would possibly hit performance. This probably isn't worth slowing down this function just so it's lazy in it's right argument (but as a gotcha now, still strict in it's left argument).

On Wed, Jan 2, 2019 at 10:50 PM V.Liepelt <[hidden email]> wrote:
> The implementation of the Ord instance for Bool is derived

So my argument would be—doesn’t this mean that we need to do cleverer deriving or at least have a hand-written instance?

> As for the justification, perhaps it's too much of a special case for only
> one value of an enumeration to compare to undefined without crashing

This is not just about crashing. (I’m using `undefined` as a way of making strictness explicit.) `False >= veryExpensiveComputation` should return `True` immediately without any unnecessary computation.

Also it doesn’t seem like a special case: this makes sense for any partially ordered Type with a top and/or bottom element.

> perhaps it inhibits optimisation opportunities.

That doesn’t seem very likely to me, I would rather think the contrary (see above): doing unnecessary work can hardly make a program run faster.

V

> On 2 Jan 2019, at 11:37, Tom Ellis <[hidden email]> wrote:
>
> On Wed, Jan 02, 2019 at 09:47:15AM +0000, V.Liepelt wrote:
>> I am surprised to find that `False <= undefined = undefined`.
>>
>> What justifies (<=) to be strict in both arguments?
>
> The implementation of the Ord instance for Bool is derived, as you can see
> here:
>
>    https://www.stackage.org/haddock/lts-12.1/ghc-prim-0.5.2.0/src/GHC-Classes.html#Ord
>
> As for the justification, perhaps it's too much of a special case for only
> one value of an enumeration to compare to undefined without crashing, and
> perhaps it inhibits optimisation opportunities.
>
> Tom
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Tom Ellis-5
In reply to this post by V.Liepelt
On Wed, Jan 02, 2019 at 11:49:40AM +0000, V.Liepelt wrote:
> > As for the justification, perhaps it's too much of a special case for only
> > one value of an enumeration to compare to undefined without crashing
>
> Also it doesn’t seem like a special case: this makes sense for any
> partially ordered Type with a top and/or bottom element.

I mean that for any data type

    data E of C1 | C2 | ...

you are preposing that the (<=) of the derived Ord instance would have a
special case for C1.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Li-yao Xia-2
In reply to this post by V.Liepelt
Hi Vilem,

 > This is not just about crashing. (I’m using `undefined` as a way of
 > making strictness explicit.) `False >= veryExpensiveComputation`
 > should return `True` immediately without any unnecessary computation.

There is also an opposite situation, where evaluating the second
argument allows us to free a lot of memory, as that argument would
otherwise remain a thunk with references to many things.

 > Also it doesn’t seem like a special case: this makes sense for any
partially ordered Type with a top and/or bottom element.

That may be acceptable with Bool because its values are small. But to
compare two pairs `(a,b) <= (x,y)` we would have to first traverse
`(a,b)` to decide whether it's the smallest element, before evaluating
the second argument to WHNF and comparing component-wise. Besides the
extra complexity (both in code and in run time), this would not be less
strict than the current default, since the first argument could get
completely evaluated before even looking at the second one: `(False,
_|_) <= (True, True) = _|_` (currently, this is `True`). We also would
not know whether the type (a, b) has a smallest element without stronger
constraints than (Ord a, Ord b), so this optimization is really only
practically feasible for types with a nullary first constructor.

Li-yao
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Sven Panne-2
In reply to this post by Tom Ellis-5
Am Mi., 2. Jan. 2019 um 15:42 Uhr schrieb Tom Ellis <[hidden email]>:
I mean that for any data type

    data E of C1 | C2 | ...

you are preposing that the (<=) of the derived Ord instance would have a
special case for C1.

... and another special case for (>=) for the last enumeration value. And a very special version for one-element enumerations. And what about (<) and (>)? And derived (==) for one-element enumerations? And, and, and... :-P

Putting on the language lawyer hat: The Haskell Report explicitly states that Bool's Ord instance is derived (section 6.1.1), and section 11.1 explicitly states that all derived operations for Eq and Ord are strict in both arguments. Consequently, Implementing Ord for Bool in a lazier way would violate the specification.

I would say that the the way the report specifies this is a good thing: Coming up with special cases is a bad design principle, consistency almost always trumps anything else (the human brain is notoriously small). Furthermore, laziness is not always a good thing, it could lead to space leaks, so e.g. making Bool's Ord operations lazier would definitely make various people very unhappy sooner or later. :-)

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Olaf Klinke
In reply to this post by V.Liepelt
Information-theoretically 'compare' must be stricter than <= because is gives more information: It decides equality, which <= doesn't. Therefore compare must be strict in both arguments. What follows is an argument that there can not be a lazy implementation of <= that behaves like logical implication.

We try to model <= after the logical implication operator. Order-theoretically, the binary operation (<=) should be antitone in the first and monotone in the second argument. The preceding sentence only makes sense once we define a mathematical order on the semantics of Bool. Let's declare the "logical" order

False < undefined < True.

I give a formal justification in Appendix A below. Arrange all nine combinations of type (Bool,Bool) in a 3x3 grid where the first dimension is descending and the second dimension is ascending in the logical order. Now we consider:

(undefined,True) must map to True
because (True,True) maps to True and descending in the first argument means ascending in the result.

(False,undefined) must map to True
because (False,False) maps to True and ascending in the second argument means ascending in the result.

Further we require (True,False) mapping to False.

But now we're in trouble: A function giving the above three return values requires ambiguous choice, which we don't have available in pure, sequential Haskell, q.e.d. It's the same reason why we can't have (&&) or (||) operators which behave symmetrically w.r.t. the logical order.

Olaf

==========
Appendix A

Let R be a binary relation on a set A. The Egli-Milner-lifting of R is a binary relation on the powerset of A.   Among several possible liftings, it is the one with the most pleasing properties [1, Theorem 2.12]. Identify the "undefined" value of a type A with the maximal element of the powerset of A, which expresses that "undefined" may evaluate to anything. In Haskell terms:

{-# LANGUAGE Rank2Types #-}
module RelationLifting where
import Prelude hiding (undefined)
type Relation a = a -> a -> Bool
type Lifting = forall a. Relation a -> Relation [a]
egliMilner :: Lifting
egliMilner r xs ys = hoare && smyth where
    hoare = all (\x -> any (\y -> r x y) ys) xs
    smyth = all (\y -> any (\x -> r x y) xs) ys
true, false, undefined :: [Bool]
true      = [True]
false     = [False]
undefined = [False,True]

RelationLifting> egliMilner (<=) false undefined
True
RelationLifting> egliMilner (<=) undefined true
True

[1] https://www.cs.le.ac.uk/people/akurz/Papers/kv-relation-lifting.pdf

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

V.Liepelt
In reply to this post by Li-yao Xia-2
Hi Li-yao,

Thanks for you interesting thoughts.

There is also an opposite situation, where evaluating the second argument allows us to free a lot of memory, as that argument would otherwise remain a thunk with references to many things.

Good point, but this is one of the tradeoffs with laziness. In the case of GHC, will the runtime not eventually free the memory of the second argument and everything it points to? It surely must do this one way or another since otherwise laziness would mean that while a process is running it will keep leaking space.

But to compare two pairs `(a,b) <= (x,y)` we would have to first traverse `(a,b)` to decide whether it's the smallest element, before evaluating the second argument to WHNF and comparing component-wise. Besides the extra complexity (both in code and in run time), this would not be less strict than the current default, since the first argument could get completely evaluated before even looking at the second one: `(False, _|_) <= (True, True) = _|_` (currently, this is `True`).

So with the laziest possible implementation (below—do check for accuracy, I might have missed something) these are the cases where the result is defined for Bool and undefined for Lazy Bool:

(F,u) <= (T,F)
(F,u) <= (T,T)
(F,u) <= (T,u)

vs. (undefined for Bool and defined for Lazy Bool)

(F,F) <= (F,u)
(F,F) <= (u,F)
(F,F) <= (u,T)
(F,F) <= (u,u)
(T,F) <= (T,u)

So it does seem that we can make it marginally more lazy overall. I’m not saying we should, I was just genuinely surprised that Ord is strict.

Definitions:

F <= _ = T
T <= q = q
F <  q = q
T < _  = F

(p, q) == (r, s) = p == r /\ q == s
(F, F) <= _ = T
(p, q) <= (r, s) = p < r \/ p == r /\ q <= s
(T, T) <  _ = F

We also would not know whether the type (a, b) has a smallest element without stronger constraints than (Ord a, Ord b), so this optimization is really only practically feasible for types with a nullary first constructor.

Hm, perhaps we are thinking about this in different ways. From the definition above, we don’t need any stronger constraints than Ord.

Best,

Vilem

On 2 Jan 2019, at 15:06, Li-yao Xia <[hidden email]> wrote:

Hi Vilem,

> This is not just about crashing. (I’m using `undefined` as a way of
> making strictness explicit.) `False >= veryExpensiveComputation`
> should return `True` immediately without any unnecessary computation.

There is also an opposite situation, where evaluating the second argument allows us to free a lot of memory, as that argument would otherwise remain a thunk with references to many things.

> Also it doesn’t seem like a special case: this makes sense for any partially ordered Type with a top and/or bottom element.

That may be acceptable with Bool because its values are small. But to compare two pairs `(a,b) <= (x,y)` we would have to first traverse `(a,b)` to decide whether it's the smallest element, before evaluating the second argument to WHNF and comparing component-wise. Besides the extra complexity (both in code and in run time), this would not be less strict than the current default, since the first argument could get completely evaluated before even looking at the second one: `(False, _|_) <= (True, True) = _|_` (currently, this is `True`). We also would not know whether the type (a, b) has a smallest element without stronger constraints than (Ord a, Ord b), so this optimization is really only practically feasible for types with a nullary first constructor.

Li-yao


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

V.Liepelt
In reply to this post by Olaf Klinke
Hi Olaf,

these are great thoughts, but are we talking about the same thing?

I was merely wondering why Ord methods are strict.

Best,

Vilem

> On 2 Jan 2019, at 21:51, Olaf Klinke <[hidden email]> wrote:
>
> Information-theoretically 'compare' must be stricter than <= because is gives more information: It decides equality, which <= doesn't. Therefore compare must be strict in both arguments. What follows is an argument that there can not be a lazy implementation of <= that behaves like logical implication.
>
> We try to model <= after the logical implication operator. Order-theoretically, the binary operation (<=) should be antitone in the first and monotone in the second argument. The preceding sentence only makes sense once we define a mathematical order on the semantics of Bool. Let's declare the "logical" order
>
> False < undefined < True.
>
> I give a formal justification in Appendix A below. Arrange all nine combinations of type (Bool,Bool) in a 3x3 grid where the first dimension is descending and the second dimension is ascending in the logical order. Now we consider:
>
> (undefined,True) must map to True
> because (True,True) maps to True and descending in the first argument means ascending in the result.
>
> (False,undefined) must map to True
> because (False,False) maps to True and ascending in the second argument means ascending in the result.
>
> Further we require (True,False) mapping to False.
>
> But now we're in trouble: A function giving the above three return values requires ambiguous choice, which we don't have available in pure, sequential Haskell, q.e.d. It's the same reason why we can't have (&&) or (||) operators which behave symmetrically w.r.t. the logical order.
>
> Olaf
>
> ==========
> Appendix A
>
> Let R be a binary relation on a set A. The Egli-Milner-lifting of R is a binary relation on the powerset of A.   Among several possible liftings, it is the one with the most pleasing properties [1, Theorem 2.12]. Identify the "undefined" value of a type A with the maximal element of the powerset of A, which expresses that "undefined" may evaluate to anything. In Haskell terms:
>
> {-# LANGUAGE Rank2Types #-}
> module RelationLifting where
> import Prelude hiding (undefined)
> type Relation a = a -> a -> Bool
> type Lifting = forall a. Relation a -> Relation [a]
> egliMilner :: Lifting
> egliMilner r xs ys = hoare && smyth where
>    hoare = all (\x -> any (\y -> r x y) ys) xs
>    smyth = all (\y -> any (\x -> r x y) xs) ys
> true, false, undefined :: [Bool]
> true      = [True]
> false     = [False]
> undefined = [False,True]
>
> RelationLifting> egliMilner (<=) false undefined
> True
> RelationLifting> egliMilner (<=) undefined true
> True
>
> [1] https://www.cs.le.ac.uk/people/akurz/Papers/kv-relation-lifting.pdf
>

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

V.Liepelt
In reply to this post by Sven Panne-2
Hi Sven,

[…] section 11.1 [of the Haskell 2010 Report] explicitly states that all derived operations for Eq and Ord are strict in both arguments.

Good idea to look at the Report. Unfortunately it doesn’t give any reasoning as to why this choice was made.

Best,

Vilem


On 2 Jan 2019, at 19:06, Sven Panne <[hidden email]> wrote:

Am Mi., 2. Jan. 2019 um 15:42 Uhr schrieb Tom Ellis <[hidden email]>:
I mean that for any data type

    data E of C1 | C2 | ...

you are preposing that the (<=) of the derived Ord instance would have a
special case for C1.

... and another special case for (>=) for the last enumeration value. And a very special version for one-element enumerations. And what about (<) and (>)? And derived (==) for one-element enumerations? And, and, and... :-P

Putting on the language lawyer hat: The Haskell Report explicitly states that Bool's Ord instance is derived (section 6.1.1), and section 11.1 explicitly states that all derived operations for Eq and Ord are strict in both arguments. Consequently, Implementing Ord for Bool in a lazier way would violate the specification.

I would say that the the way the report specifies this is a good thing: Coming up with special cases is a bad design principle, consistency almost always trumps anything else (the human brain is notoriously small). Furthermore, laziness is not always a good thing, it could lead to space leaks, so e.g. making Bool's Ord operations lazier would definitely make various people very unhappy sooner or later. :-)
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Sven Panne-2
Am Fr., 4. Jan. 2019 um 16:55 Uhr schrieb V.Liepelt <[hidden email]>:
Hi Sven,

[…] section 11.1 [of the Haskell 2010 Report] explicitly states that all derived operations for Eq and Ord are strict in both arguments.

Good idea to look at the Report. Unfortunately it doesn’t give any reasoning as to why this choice was made.

As I said: Consistency. (Well, I didn't write the report, but this seems to be the most obvious reason.)

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Sven Panne-2
In reply to this post by V.Liepelt
Am Fr., 4. Jan. 2019 um 16:46 Uhr schrieb V.Liepelt <[hidden email]>:
[...] Good point, but this is one of the tradeoffs with laziness. In the case of GHC, will the runtime not eventually free the memory of the second argument and everything it points to? It surely must do this one way or another since otherwise laziness would mean that while a process is running it will keep leaking space.

You *will* leak space if you keep an unevaluated argument around for a long time, there is nothing any implementation can really do about it: It can't know for sure if you will eventually throw away that argument or (partially) evaluate it. Sometimes the optimizer (e.g. via strictness analysis) can help, but not in the general case. So making an argument lazier is not a no-brainer, quite the opposite...

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Viktor Dukhovni
> On Jan 4, 2019, at 11:47 AM, Sven Panne <[hidden email]> wrote:
>
> You *will* leak space if you keep an unevaluated argument around for a long time, there is nothing any implementation can really do about it: It can't know for sure if you will eventually throw away that argument or (partially) evaluate it. Sometimes the optimizer (e.g. via strictness analysis) can help, but not in the general case. So making an argument lazier is not a no-brainer, quite the opposite...

Only if it is repeatedly used in ever deeper unevaluated expressions,
such as repeatedly incrementing an IORef counter, without ever forcing
the value.

In the case of a lazy function ignoring its argument, no space is leaked
unless that argument is retained elsewhere, and the function was the sole
means of forcing the value.  Unreferenced unevaluated thunks get GC'd.
Space leaks require ever deeper chains of unevaluated thunks.

If laziness always leaked Haskell would not work terribly well.  I have
code that runs for ~9 hours in constant memory allocating and freeing
around 13TB of memory over its lifetime.  Various functions it calls
do some lazy evaluation or other, and while in some cases forcing the
values that are sure to get used might reduce GC activity, there's no
space leak.

--
        Viktor.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Ord methods too strict?

Sven Panne-2
Am Fr., 4. Jan. 2019 um 18:24 Uhr schrieb Viktor Dukhovni <[hidden email]>:
[...] In the case of a lazy function ignoring its argument, no space is leaked
unless that argument is retained elsewhere, and the function was the sole
means of forcing the value.

This is the scenario I had in mind, but obviously I didn't explain that terribly well... :-}  Personally, I think this is not so uncommon, at least in the initial stages of writing a library or program.
 
[...] Space leaks require ever deeper chains of unevaluated thunks. [...]

Perhaps we have different definitions of  "space leak" (is there an "official" one?), but keeping a single thunk alive for a long time, which in turn keeps some huge data structure alive is a kind of leak, too, no deep chains involved. Maybe there is a better term describing this situation.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.