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. |
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`. _______________________________________________ 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. |
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
_______________________________________________ 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. |
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. |
> 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. |
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 _______________________________________________ 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. |
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!)
Isn’t “asymmetry” the whole point of laziness? Consider `(||)`.
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
_______________________________________________ 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. |
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. |
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. |
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 ... 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. |
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. |
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
_______________________________________________ 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. |
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. |
In reply to this post by Sven Panne-2
Hi Sven,
Good idea to look at the Report. Unfortunately it doesn’t give any reasoning as to
why this choice was made.
Best,
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. |
Am Fr., 4. Jan. 2019 um 16:55 Uhr schrieb V.Liepelt <[hidden email]>:
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. |
In reply to this post by V.Liepelt
Am Fr., 4. Jan. 2019 um 16:46 Uhr schrieb V.Liepelt <[hidden email]>:
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. |
> 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. |
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 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. |
Free forum by Nabble | Edit this page |