
Hello all, As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11 we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a) and a function that returns a list of all the paths (which are lists of node values) where each path element makes the predicate true. findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath pred lf rtpaths = findAllPath pred rt in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing lfpaths then Just (map (r:) $ fromJust rtpaths) else if isNothing rtpaths then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing Later on we noticed that this could be simply written as: findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = [] without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments? 2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments? Cheers, -- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK

Hi
findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = []
without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments?
Because in all call paths findAllPath will call g with its second argument. g will always evaluate (by pattern matching on) its value argument.
2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments?
Yes, strictness analysis is a very well studied subject - http://haskell.org/haskellwiki/Research_papers/Compilation#Strictness . Essentially, an argument is strict if passing _|_ for that value results in _|_. So to take your example, evaluating: findAllPath a _|_ g _|_ _|_ Since g tests what value _|_ has, we get bottom. Thanks Neil

Roberto Zunino wrote:
Neil Mitchell wrote:
is there any automated way to know when a function is strict in its arguments?
Yes, strictness analysis is a very well studied subject -
...and is undecidable, in general. ;-)
*thinks* Conjecture #1: All nontrivial properties of a computer program are undecidable in general. *thinks more* Conjecture #2: Conjecture #1 is undecidable...

Andrew Coppin wrote:
*thinks*
Conjecture #1: All nontrivial properties of a computer program are undecidable in general.
That is the well-known Rice's theorem. (A very handy one in exams about theoretical computer science, since you can smash so many questions with "follows from Rice").
*thinks more*
Conjecture #2: Conjecture #1 is undecidable...
But the question wether a nontrivial property of a computer program is decidable is *not* a property of computer programs itself. (it is a property of properties of computer programs instead). Rice's theorem doesn't apply to Rice's theorem. (Thats the problem with smashing everything with Rice's theorem: it may be not applicable). Tillmann

Tillmann Rendel wrote:
Andrew Coppin wrote:
*thinks*
Conjecture #1: All nontrivial properties of a computer program are undecidable in general.
That is the well-known Rice's theorem.
Wait - Rice's *theorem*? So Rice *proved* this? OMG, I was *right* about something! :-D
Conjecture #2: Conjecture #1 is undecidable... *thinks more*
But the question wether a nontrivial property of a computer program is decidable is *not* a property of computer programs itself.
Indeed no. And, in fact, if Rice's theorem has been proved, then clearly it *is* decidable. And has been decided. I was merely noting that questions of the form "is X decidable?" are usually undecidable. (It's as if God himself wants to tease us...)

On Dec 5, 2007 11:56 AM, Andrew Coppin
I was merely noting that questions of the form "is X decidable?" are usually undecidable. (It's as if God himself wants to tease us...)
I take issue with your definition of "usually" then. Whenever "X is decidable" is undecidable, "'X is decidable' is decidable' is decidable, namely false. So there are at least as many decidable sentences of the form "X is decidable" as there are undecidable ones. Luke

Luke Palmer wrote:
On Dec 5, 2007 11:56 AM, Andrew Coppin
wrote: I was merely noting that questions of the form "is X decidable?" are usually undecidable. (It's as if God himself wants to tease us...)
I take issue with your definition of "usually" then.
Whenever "X is decidable" is undecidable, "'X is decidable' is decidable' is decidable, namely false. So there are at least as many decidable sentences of the form "X is decidable" as there are undecidable ones.
Ouch... my head hurts. OK, well how about I rephrase it as "most 'interesting' questions about decidability tend to be undecidable" and we call it quits? ;-)

On Dec 5, 2007 12:30 PM, Andrew Coppin
Luke Palmer wrote:
On Dec 5, 2007 11:56 AM, Andrew Coppin
wrote: I was merely noting that questions of the form "is X decidable?" are usually undecidable. (It's as if God himself wants to tease us...)
I take issue with your definition of "usually" then.
Whenever "X is decidable" is undecidable, "'X is decidable' is decidable' is decidable, namely false. So there are at least as many decidable sentences of the form "X is decidable" as there are undecidable ones.
Ouch... my head hurts.
OK, well how about I rephrase it as "most 'interesting' questions about decidability tend to be undecidable" and we call it quits? ;-)
Nah, I was just performing a slight-of-hand on you. Basically by saying "X is decidable" is undecidable, you were implying you could prove it. Which you usually can't. Well, rather, which you usually don't know if you can... Luke

On Dec 4, 2007 10:00 PM, Neil Mitchell
Hi
findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = []
without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments?
Because in all call paths findAllPath will call g with its second argument. g will always evaluate (by pattern matching on) its value argument.
Wait! You're analyzing my second function and you're saying that it is strict in its arguments? Gee, that's bad. I questioned about the first one. The second seems to be definitely lazy because I can use it on such big trees like I showed. How come I can do this computation if like you said the function is strict?
2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments?
Yes, strictness analysis is a very well studied subject - http://haskell.org/haskellwiki/Research_papers/Compilation#Strictness . Essentially, an argument is strict if passing _|_ for that value results in _|_. So to take your example, evaluating:
findAllPath a _|_ g _|_ _|_
Since g tests what value _|_ has, we get bottom.
Thanks
Neil
-- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK

On Tue, Dec 04, 2007 at 09:41:36PM +0000, Paulo J. Matos wrote:
Hello all,
As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11
we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)
and a function that returns a list of all the paths (which are lists of node values) where each path element makes the predicate true. findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath pred lf rtpaths = findAllPath pred rt in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing lfpaths then Just (map (r:) $ fromJust rtpaths) else if isNothing rtpaths then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing
Later on we noticed that this could be simply written as: findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = []
without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments?
Because of the definition of strictness. A function is strict iff f undefined = undefined. findAllPath pred undefined -> undefined because of the case analysis findAllPath undefined (Leaf _) -> undefined because pred is applied in the guard findAllPath undefined Branch{} -> undefined because pred is applied in the guard
2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments?
No, because this is in general equivalent to the halting problem: f _ = head [ i | i <- [1,3.], i == sum [ k | k <- [1..i-1], i `mod` k == 0 ] ] f is strict iff there do not exist odd perfect numbers. However, fairly good conservative approximations exist, for instance in the GHC optimizer - compile your code with -ddump-simpl to see (among other things) a dump of the strictness properties determined. (use -O, of course) Stefan

Is there a reason why strictness is defined as
f _|_ = _|_
instead of, for example,
forall x :: Exception. f (throw x) = throw x where an exception thrown from pure code is observable in IO.
In the second case we need to prove that the argument is evaluated at some
point, which is also equivalent to the halting problem but more captures the
notion of "f evaluates its argument" rather than "either f evaluates its
argument, or f _ is _|_"
I suppose the first case allows us to do more eager evaluation; but are
there a lot of cases where that matters?
-- ryan
On 12/4/07, Stefan O'Rear
Hello all,
As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11
we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)
and a function that returns a list of all the paths (which are lists of node values) where each path element makes the predicate true. findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath
On Tue, Dec 04, 2007 at 09:41:36PM +0000, Paulo J. Matos wrote: pred lf
rtpaths = findAllPath
pred rt
in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing lfpaths then Just (map (r:) $ fromJust rtpaths) else if isNothing
rtpaths
then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing
Later on we noticed that this could be simply written as: findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = []
without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments?
Because of the definition of strictness. A function is strict iff f undefined = undefined.
findAllPath pred undefined -> undefined because of the case analysis findAllPath undefined (Leaf _) -> undefined because pred is applied in the guard findAllPath undefined Branch{} -> undefined because pred is applied in the guard
2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments?
No, because this is in general equivalent to the halting problem:
f _ = head [ i | i <- [1,3.], i == sum [ k | k <- [1..i-1], i `mod` k == 0 ] ]
f is strict iff there do not exist odd perfect numbers.
However, fairly good conservative approximations exist, for instance in the GHC optimizer - compile your code with -ddump-simpl to see (among other things) a dump of the strictness properties determined. (use -O, of course)
Stefan
-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux)
iD8DBQFHVc/eFBz7OZ2P+dIRAmJKAKCDPQl1P5nYNPBOoR6isw9rAg5XowCgwI1s 02/+pzXto1YRiXSSslZsmjk= =7dDj -----END PGP SIGNATURE-----
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Tue, Dec 04, 2007 at 03:07:01PM -0800, Ryan Ingram wrote:
Is there a reason why strictness is defined as
f _|_ = _|_
instead of, for example,
forall x :: Exception. f (throw x) = throw x where an exception thrown from pure code is observable in IO.
In the second case we need to prove that the argument is evaluated at some point, which is also equivalent to the halting problem but more captures the notion of "f evaluates its argument" rather than "either f evaluates its argument, or f _ is _|_"
I suppose the first case allows us to do more eager evaluation; but are there a lot of cases where that matters?
"Is there a reason why 2 + 2 is defined as 4 instead of, for example, 5?" Strictness is more useful in practice, simpler to define, and easier to approximate. What benefit does your notion offer? Stefan

On 12/4/07, Stefan O'Rear
"Is there a reason why 2 + 2 is defined as 4 instead of, for example, 5?"
Wow. That wasn't really necessary. 4 has a clear meaning (the number after the number after the number after the number after zero) which is equivalent to 2 + 2. I'm not talking about naming issues; you could say that 5 was that number but then nobody would know what you are talking about. I am asking about the history & motivation behind the original definition of strictness, not arguing for a redefinition. Strictness is more useful in practice, simpler to define, and easier to
approximate.
Please elaborate; this is exactly why I asked. In particular, "more useful in practice" is the thing I am most curious about.
What benefit does your notion offer?
Well, one usually says something like "f is strict in its 2nd argument" which on casual reading tends to make me think that it has something to do with the argument. By the actual definition, however, f _ _ = undefined is strict in all of its arguments; but it's clear from the definition that the arguments are irrelevant. -- ryan

On Tue, Dec 04, 2007 at 03:35:28PM -0800, Ryan Ingram wrote:
On 12/4/07, Stefan O'Rear
wrote: "Is there a reason why 2 + 2 is defined as 4 instead of, for example, 5?"
Wow. That wasn't really necessary. 4 has a clear meaning (the number after the number after the number after the number after zero) which is equivalent to 2 + 2. I'm not talking about naming issues; you could say that 5 was that number but then nobody would know what you are talking about. I am asking about the history & motivation behind the original definition of strictness, not arguing for a redefinition.
Oh. Sorry.
Strictness is more useful in practice, simpler to define, and easier to approximate.
Please elaborate; this is exactly why I asked. In particular, "more useful in practice" is the thing I am most curious about.
When you see an expression of the form: f a you generally want to evaluate a before applying; but if a is _|_, this will only give the correct result if f a = _|_. Merely 'guaranteed to evaluate' misses out on some common cases, for instance ifac: ifac 0 a = a ifac n a = ifac (n - 1) (a * n) ifac is guaranteed to either evaluate a, or go into an infinite loop - so it can be found strict, and unboxed. Whereas 'ifac -1 (error "moo")' is an infinite loop, so using a definition based on evaluation misses this case.
What benefit does your notion offer?
Well, one usually says something like "f is strict in its 2nd argument" which on casual reading tends to make me think that it has something to do with the argument. By the actual definition, however, f _ _ = undefined is strict in all of its arguments; but it's clear from the definition that the arguments are irrelevant.
Stefan

On 12/4/07, Stefan O'Rear
When you see an expression of the form:
f a
you generally want to evaluate a before applying; but if a is _|_, this will only give the correct result if f a = _|_. Merely 'guaranteed to evaluate' misses out on some common cases, for instance ifac:
ifac 0 a = a ifac n a = ifac (n - 1) (a * n)
ifac is guaranteed to either evaluate a, or go into an infinite loop - so it can be found strict, and unboxed. Whereas 'ifac -1 (error "moo")' is an infinite loop, so using a definition based on evaluation misses this case.
By this line: you generally want to evaluate a before applying; but if a is _|_, this will only give the correct result if f a = _|_ I assume you mean that it's generally more efficient to do things that way, because the calling function may have more information about "a" or how it is calculated, so you may be able to optimize better by doing eager evaluation whenever it is correct. Your ifac example makes perfect sense, thanks. -- ryan

On Tue, Dec 04, 2007 at 07:43:36PM -0800, Ryan Ingram wrote:
On 12/4/07, Stefan O'Rear
wrote: When you see an expression of the form:
f a
you generally want to evaluate a before applying; but if a is _|_, this will only give the correct result if f a = _|_. Merely 'guaranteed to evaluate' misses out on some common cases, for instance ifac:
ifac 0 a = a ifac n a = ifac (n - 1) (a * n)
ifac is guaranteed to either evaluate a, or go into an infinite loop - so it can be found strict, and unboxed. Whereas 'ifac -1 (error "moo")' is an infinite loop, so using a definition based on evaluation misses this case.
By this line: you generally want to evaluate a before applying; but if a is _|_, this will only give the correct result if f a = _|_
I assume you mean that it's generally more efficient to do things that way, because the calling function may have more information about "a" or how it is calculated, so you may be able to optimize better by doing eager evaluation whenever it is correct.
Yes - if we know that a value is needed, eager evaluation is more efficient, because no time need be spent constructing and deconstructing expressions in memory. More significantly, strictness facilitates certain unboxing transformations. Since ifac is strict, (optimized) code will never call it with anything except a concrete number, so we can gainfully specialize it to the case of a pre-evaluated argument; so instead of passing pointer-to-Int-node, we can just pass a raw machine integer. With a few passes of standard compilation technology (inlining +, etc) we wind up with the moral equivalent of while (n--) { i *= n; }.
Your ifac example makes perfect sense, thanks.
Stefan

Hasn't Ryan raised an interesting point, though? Bottom is used to denote non-termination and run-time errors. Are they the same thing? To me, they're not. A non-terminating program has different behaviour from a failing program. When it comes to strictness, the concept is defined in a particular semantic context, typically an applicative structure: [[ f x ]] = App [[f]] [[x]] Function f is strict if App [[f]] _|_ = _|_ Yet, that definition is pinned down in a semantics where what _|_ models is clearly defined. I don't see why one could not provide a more detailed semantics where certain kinds of run-time errors are distinguished from bottom. Actually, this already happens. Type systems are there to capture many program properties statically. Some properties that can't be captured statically are captured dynamically: the compiler introduces run-time tests. Checking for non-termination is undecidable, but putting run-time checks for certain errors is not.

See http://doi.acm.org/10.1145/301631.301637 and http://dx.doi.org/10.1016/S1571-0661(05)80288-9 Pablo Nogueira wrote:
Hasn't Ryan raised an interesting point, though?
Bottom is used to denote non-termination and run-time errors. Are they the same thing? To me, they're not. A non-terminating program has different behaviour from a failing program.
When it comes to strictness, the concept is defined in a particular semantic context, typically an applicative structure:
[[ f x ]] = App [[f]] [[x]]
Function f is strict if App [[f]] _|_ = _|_
Yet, that definition is pinned down in a semantics where what _|_ models is clearly defined.
I don't see why one could not provide a more detailed semantics where certain kinds of run-time errors are distinguished from bottom. Actually, this already happens. Type systems are there to capture many program properties statically. Some properties that can't be captured statically are captured dynamically: the compiler introduces run-time tests. Checking for non-termination is undecidable, but putting run-time checks for certain errors is not. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

On Wed, 2007-12-05 at 10:01 +0100, Pablo Nogueira wrote:
Hasn't Ryan raised an interesting point, though?
Bottom is used to denote non-termination and run-time errors. Are they the same thing?
Up to observational equality, yes.
To me, they're not. A non-terminating program has different behaviour from a failing program.
When it comes to strictness, the concept is defined in a particular semantic context, typically an applicative structure:
[[ f x ]] = App [[f]] [[x]]
Function f is strict if App [[f]] _|_ = _|_
Yet, that definition is pinned down in a semantics where what _|_ models is clearly defined.
I don't see why one could not provide a more detailed semantics where certain kinds of run-time errors are distinguished from bottom.
When there is reason to, that is exactly what is done. The domain grows from 1+V to 1+V+E. However, when run-time errors can be observed you start having to provide answers to undesirable questions: what is the behavior of error "foo" + error "bar"? Another person has pointed you to the imprecise exceptions paper that gives one well thought out answer for this in the context of Haskell.
Actually, this already happens. Type systems are there to capture many program properties statically. Some properties that can't be captured statically are captured dynamically: the compiler introduces run-time tests. Checking for non-termination is undecidable, but putting run-time checks for certain errors is not. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Tue, Dec 04, 2007 at 03:35:28PM -0800, Ryan Ingram wrote:
On 12/4/07, Stefan O'Rear
wrote: Well, one usually says something like "f is strict in its 2nd argument" which on casual reading tends to make me think that it has something to do with the argument. By the actual definition, however, f _ _ = undefined is strict in all of its arguments; but it's clear from the definition that the arguments are irrelevant.
this becomes more clear if you translate strictness into a logical representation. f x y = z saying f is strict in y is equivalent to y diverges implies z diverges. note that this is a one way implication. so, if z diverges, then the implication is trivially satisfied, as it is if y doesn't diverge, however if y diverges then z must diverge and that is what strictness means. or equivalantly z diverges \/ ! y diverges for an example of why this is useful think of the following imagine we know we are applying a function f to _|_, and we know f is strict in its first argument. Knowing it is strict, we can elide the call to f altogether and return bottom immediately. this is true whether f examines it's argument or not, since f _|_ = _|_ and we know we are passing _|_ then we can just return _|_. This is one of many optimizations that 'strictness analysis' allows. John * note, I am using 'x diverges' and 'x is bottom' to mean the same thing. Not all agree this is correct usage, even sometimes I don't. but for the purposes of this it is fine IMHO. -- John Meacham - ⑆repetae.net⑆john⑈

I don't even understand what your notation means.
But apart from that, there are good reasons to define strictness
denotationally instead of operationally. Remember that _|_ is not only
exceptions, but also non-termination.
For instance, the following function is strict without using its argument:
f x = f x
because
f _|_ = _|_
-- Lennart
On Dec 4, 2007 11:07 PM, Ryan Ingram
Is there a reason why strictness is defined as
f _|_ = _|_
instead of, for example,
forall x :: Exception. f (throw x) = throw x where an exception thrown from pure code is observable in IO.
In the second case we need to prove that the argument is evaluated at some point, which is also equivalent to the halting problem but more captures the notion of "f evaluates its argument" rather than "either f evaluates its argument, or f _ is _|_"
I suppose the first case allows us to do more eager evaluation; but are there a lot of cases where that matters?
-- ryan
On 12/4/07, Stefan O'Rear
wrote: Hello all,
As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11
we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)
and a function that returns a list of all the paths (which are lists of node values) where each path element makes the predicate true. findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath
On Tue, Dec 04, 2007 at 09:41:36PM +0000, Paulo J. Matos wrote: pred lf
rtpaths = findAllPath
pred rt
in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing
lfpaths
then Just (map (r:) $ fromJust rtpaths) else if isNothing
rtpaths
then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing
Later on we noticed that this could be simply written as: findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = []
without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments?
Because of the definition of strictness. A function is strict iff f undefined = undefined.
findAllPath pred undefined -> undefined because of the case analysis findAllPath undefined (Leaf _) -> undefined because pred is applied in the guard findAllPath undefined Branch{} -> undefined because pred is applied in the guard
2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments?
No, because this is in general equivalent to the halting problem:
f _ = head [ i | i <- [1,3.], i == sum [ k | k <- [1..i-1], i `mod` k == 0 ] ]
f is strict iff there do not exist odd perfect numbers.
However, fairly good conservative approximations exist, for instance in the GHC optimizer - compile your code with -ddump-simpl to see (among other things) a dump of the strictness properties determined. (use -O, of course)
Stefan
-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux)
iD8DBQFHVc/eFBz7OZ2P+dIRAmJKAKCDPQl1P5nYNPBOoR6isw9rAg5XowCgwI1s 02/+pzXto1YRiXSSslZsmjk= =7dDj -----END PGP SIGNATURE-----
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Tue, Dec 04, 2007 at 03:07:01PM -0800, Ryan Ingram wrote:
Is there a reason why strictness is defined as
f _|_ = _|_
instead of, for example,
forall x :: Exception. f (throw x) = throw x
There's discussion along these lines in http://hackage.haskell.org/trac/ghc/ticket/1171 Thanks Ian

Ian Lynagh wrote:
On Tue, Dec 04, 2007 at 03:07:01PM -0800, Ryan Ingram wrote:
Is there a reason why strictness is defined as
f _|_ = _|_
instead of, for example,
forall x :: Exception. f (throw x) = throw x
There's discussion along these lines in http://hackage.haskell.org/trac/ghc/ticket/1171
Gotta love bug reports where nobody is even sure what the "correct" behaviour actually *is*... ;-)

On Fri, 7 Dec 2007, Andrew Coppin wrote:
Ian Lynagh wrote:
On Tue, Dec 04, 2007 at 03:07:01PM -0800, Ryan Ingram wrote:
Is there a reason why strictness is defined as
f _|_ = _|_
instead of, for example,
forall x :: Exception. f (throw x) = throw x
Errors and exceptions are two very different concepts.

On 2007-12-04, Paulo J. Matos
Hello all,
As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11
we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)
Totally avoiding your question, but I'm curious as to why you deliberately exclude empty trees. Come to think of it, how can you represent a tree with two elements? Wouldn't
data BTree a = Empty | Branch (BTree a) a (BTree a)
be better? -- Aaron Denney -><-

On Dec 5, 2007 12:16 AM, Aaron Denney
we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)
Totally avoiding your question, but I'm curious as to why you deliberately exclude empty trees.
Come to think of it, how can you represent a tree with two elements?
Indeed, this tree is only capable of representing odd numbers of elements, which can be shown by straightforward induction. Luke

On Dec 5, 2007 12:16 AM, Aaron Denney
On 2007-12-04, Paulo J. Matos
wrote: Hello all,
As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11
we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)
Totally avoiding your question, but I'm curious as to why you deliberately exclude empty trees.
Come to think of it, how can you represent a tree with two elements?
Good question. I think we were just trying to define a tree in the meeting and everyone agreed on this representation.
Wouldn't
data BTree a = Empty | Branch (BTree a) a (BTree a)
be better?
Possibly :) I think that at the time nobody really cared about empty trees! But for a really application we would have had to define them probably. Now thinking about it, it seems like defining lists without Null, strange, isn't it?
-- Aaron Denney -><-
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK

Paulo J. Matos wrote:
Hello all,
Hi.
findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath pred lf rtpaths = findAllPath pred rt in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing lfpaths then Just (map (r:) $ fromJust rtpaths) else if isNothing rtpaths then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing
Ignoring the fact that you found a better way to write this entirely, a style point. Use of isNothing and fromJust and a cascade of ifs is generally a poor sign, much better to use case: findAllPath pred (Branch lf r rt) | pred r = case (findAllPath pred lf,findAllPath pred rt) of (Nothing,Nothing) -> Nothing (Nothing,Just rtpaths) -> Just (map (r:) rtpaths) (Just lfpaths,Nothing) -> Just (map (r:) lfpaths) (Just lfpaths,Just rtpaths) -> Just (map (r:) $ rtpaths ++ lfpaths) | otherwise = Nothing the general pattern is : replace isNothing with a case match on Nothing, replace fromJust with a case match on Just, don't be afraid to case two expressions at once. Hope someone finds that useful, Jules

On Dec 5, 2007 10:44 AM, Jules Bean
Paulo J. Matos wrote:
Hello all,
Hi.
findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath pred lf rtpaths = findAllPath pred rt in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing lfpaths then Just (map (r:) $ fromJust rtpaths) else if isNothing rtpaths then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing
Ignoring the fact that you found a better way to write this entirely, a style point.
Use of isNothing and fromJust and a cascade of ifs is generally a poor sign, much better to use case:
findAllPath pred (Branch lf r rt) | pred r = case (findAllPath pred lf,findAllPath pred rt) of (Nothing,Nothing) -> Nothing (Nothing,Just rtpaths) -> Just (map (r:) rtpaths) (Just lfpaths,Nothing) -> Just (map (r:) lfpaths) (Just lfpaths,Just rtpaths) -> Just (map (r:) $ rtpaths ++ lfpaths) | otherwise = Nothing
the general pattern is : replace isNothing with a case match on Nothing, replace fromJust with a case match on Just, don't be afraid to case two expressions at once.
Hope someone finds that useful,
Thanks, Although I think that the general thread diverged from my initial question, here it is again, why is this terrible function (I know it is ugly) evaluating all of the resulting list when I just request the head? (at seems from my experiments that's what it seems to be doing). BTW, I thought that the problem of " evaluating all of the resulting list when I just request the head " was related to argument strictness but from the other mails, I think I was wrong. :)
Jules
-- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK

Use of isNothing and fromJust and a cascade of ifs is generally a poor sign, much better to use case:
findAllPath pred (Branch lf r rt) | pred r = case (findAllPath pred lf,findAllPath pred rt) of (Nothing,Nothing) -> Nothing (Nothing,Just rtpaths) -> Just (map (r:) rtpaths) (Just lfpaths,Nothing) -> Just (map (r:) lfpaths) (Just lfpaths,Just rtpaths) -> Just (map (r:) $ rtpaths ++ lfpaths) | otherwise = Nothing
the general pattern is : replace isNothing with a case match on Nothing, replace fromJust with a case match on Just, don't be afraid to case two expressions at once.
Nested Maybe cases put me in mind of the Maybe monad. Although in this case it''s not trivial; we also need to involve the Maybe [a] instance of Data.Monoid too (for the mappend function). I do wonder if I'm abusing the monadic instances of Maybe though; is this really any clearer than Jules' code? (BTW, this has probably come up before, but wouldn't it be a little bit nicer if "when" returned mzero rather than () in the "do nothing" case?)
when' :: MonadPlus m => Bool -> m a -> m a when' pred action = if pred then action else mzero
findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) = when' (pred l) (return [[l]]) findAllPath pred (Branch lf r rt) = when' (pred r) $ do x <- mappend (findAllPath pred lf) (findAllPath pred rt) return (map (r:) x)
Alistair

On Dec 6, 2007 9:30 AM, Alistair Bayley
Use of isNothing and fromJust and a cascade of ifs is generally a poor sign, much better to use case:
findAllPath pred (Branch lf r rt) | pred r = case (findAllPath pred lf,findAllPath pred rt) of (Nothing,Nothing) -> Nothing (Nothing,Just rtpaths) -> Just (map (r:) rtpaths) (Just lfpaths,Nothing) -> Just (map (r:) lfpaths) (Just lfpaths,Just rtpaths) -> Just (map (r:) $ rtpaths ++ lfpaths) | otherwise = Nothing
the general pattern is : replace isNothing with a case match on Nothing, replace fromJust with a case match on Just, don't be afraid to case two expressions at once.
I have actually seen this pattern a lot recently. Recently I have started using a function: mergeMaybes :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a mergeMaybes f Nothing y = y mergeMaybes f x Nothing = x mergeMaybes f (Just x) (Just y) = Just (f x y) With which findAllPath could be written: finaAllPath pred (Branch lf r rt) | pred r = fmap (map (r:)) $ mergeMaybes (++) (findAllPath lf) (findAllPath rt) | otherwise = Nothing Or this more search-like feel: findAllPath pred (Branch lf r rt) = do guard (pred r) subpaths <- mergeMaybes (++) (findAllPath lf) (findAllPath rt) return $ map (r:) subpaths Luke

On 12/6/07, Luke Palmer
I have actually seen this pattern a lot recently. Recently I have started using a function:
mergeMaybes :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a mergeMaybes f Nothing y = y mergeMaybes f x Nothing = x mergeMaybes f (Just x) (Just y) = Just (f x y)
mergeMaybes = liftM2 -- from Control.Monad

On 12/6/07, Ryan Ingram
On 12/6/07, Luke Palmer
wrote: I have actually seen this pattern a lot recently. Recently I have started using a function:
mergeMaybes :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a mergeMaybes f Nothing y = y mergeMaybes f x Nothing = x mergeMaybes f (Just x) (Just y) = Just (f x y)
mergeMaybes = liftM2 -- from Control.Monad
Oh wait, not quite. Didn't realize you were returning the intermediate values in the "not nothing" case. mergeMaybes f x y = liftM2 f `mplus` x `mplus` y

Alistair Bayley wrote:
Nested Maybe cases put me in mind of the Maybe monad. Although in this case it''s not trivial; we also need to involve the Maybe [a] instance of Data.Monoid too (for the mappend function). I do wonder if I'm abusing the monadic instances of Maybe though; is this really any clearer than Jules' code?
I think the 'right' answer for this case is to drop the maybes and just use lists, which is what the OP himself realised. I often find that if I think I want a Monoid instance for Maybe [a], what I really want is to just use [a]. (Not always of course...).
(BTW, this has probably come up before, but wouldn't it be a little bit nicer if "when" returned mzero rather than () in the "do nothing" case?)
Yes and no. I've wanted your when' once or twice, but the return () version is useful too... Jules

Jules Bean wrote:
I think the 'right' answer for this case is to drop the maybes and just use lists, which is what the OP himself realised.
Yes, part of the fun of programming is when you realize that you have been re-implementing the right data type inside of a wrong one. Alistair Bayley wrote:
(BTW, this has probably come up before, but wouldn't it be a little bit nicer if "when" returned mzero rather than () in the "do nothing" case?)
No. We already have both of those: when pred action guard pred >> action -Yitz

I'm glad that my initial post generated such an interesting discussion but I'm still not understanding why the first version of findAllPath seems to be computing the whole list even when I just request the head, while the second one doesn't. I thought that this was denominated by "findAllPath is strict in its arguments" but it seems that I haven't used the right terminology to explain what I really wanted to understand. -- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK

Hi Paolo,
On Dec 5, 2007 2:09 PM, Paulo J. Matos
I'm glad that my initial post generated such an interesting discussion but I'm still not understanding why the first version of findAllPath seems to be computing the whole list even when I just request the head, while the second one doesn't.
Because the function starts its work with if isNothing lfpaths && isNothing rtpaths then Nothing else ... which forces the evaluation of 'lfpaths' and 'rtpaths' to see whether they are Just or Nothing, which recursively forces the evaluation of findAllPath for the whole tree. Hope this helps, - Benja

On Dec 5, 2007 1:43 PM, Benja Fallenstein
Hi Paolo,
On Dec 5, 2007 2:09 PM, Paulo J. Matos
wrote: I'm glad that my initial post generated such an interesting discussion but I'm still not understanding why the first version of findAllPath seems to be computing the whole list even when I just request the head, while the second one doesn't.
Because the function starts its work with
if isNothing lfpaths && isNothing rtpaths then Nothing else ...
which forces the evaluation of 'lfpaths' and 'rtpaths' to see whether they are Just or Nothing, which recursively forces the evaluation of findAllPath for the whole tree.
Oh, but lfpaths is not nothing so that means that isNothing rtpaths shouldn't be evaluated, right?
Hope this helps, - Benja
-- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK

On Dec 5, 2007 5:40 PM, Paulo J. Matos
Oh, but lfpaths is not nothing so that means that isNothing rtpaths shouldn't be evaluated, right?
You're right, and I was stupid not to think about that case. Since Luke already gave an in-depth analysis I'll be quiet now :-) - Benja

On Dec 4, 2007 9:41 PM, Paulo J. Matos
Hello all,
As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11
we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)
and a function that returns a list of all the paths (which are lists of node values) where each path element makes the predicate true. findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath pred lf rtpaths = findAllPath pred rt in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing lfpaths then Just (map (r:) $ fromJust rtpaths) else if isNothing rtpaths then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing
I don't think this evaluates the whole tree every time, but it certainly evaluates more than it needs to. It has to do with an extra check. Here's a very operational description: First note that if findAllPath returns Nothing, then it has evaluated the tree down to the contour where all the preds are false. Let's suppose that this is the best possible case, where there is a path down the left side of the tree with no backtracking where all nodes are true. findAllPath pred (Leaf l) = Just [[l]] Now: if isNothing lfpaths && ... -- false already, lfpaths is a Just, go to else branch else if isNothing lfpaths ... -- false again, go to else branch else if isNothing rtpaths ... To check this, you have to evaluate rtpaths down to its false contour before you can proceed. You didn't need to do this. Instead, writing the last else as: else Just (map (r:) $ fromJust lfpaths ++ fromMaybe [] rtpaths) Will get you behavior -- I think -- equivalent to the original. Except for that it will return paths in leftmost order rather than rightmost. But changing the order of some of those checks will get you back the original rightmost behavior and lazy semantics. Left as an exercise for the OP :-) Luke
Later on we noticed that this could be simply written as: findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = []
without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments? 2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments?
Cheers,
-- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Dec 5, 2007 1:51 PM, Luke Palmer
On Dec 4, 2007 9:41 PM, Paulo J. Matos
wrote: Hello all,
As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11
we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)
and a function that returns a list of all the paths (which are lists of node values) where each path element makes the predicate true. findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath pred lf rtpaths = findAllPath pred rt in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing lfpaths then Just (map (r:) $ fromJust rtpaths) else if isNothing rtpaths then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing
I don't think this evaluates the whole tree every time, but it certainly evaluates more than it needs to. It has to do with an extra check. Here's a very operational description:
First note that if findAllPath returns Nothing, then it has evaluated the tree down to the contour where all the preds are false. Let's suppose that this is the best possible case, where there is a path down the left side of the tree with no backtracking where all nodes are true.
findAllPath pred (Leaf l) = Just [[l]]
Now:
if isNothing lfpaths && ... -- false already, lfpaths is a Just, go to else branch else if isNothing lfpaths ... -- false again, go to else branch else if isNothing rtpaths ...
To check this, you have to evaluate rtpaths down to its false contour before you can proceed. You didn't need to do this. Instead, writing the last else as:
else Just (map (r:) $ fromJust lfpaths ++ fromMaybe [] rtpaths)
Will get you behavior -- I think -- equivalent to the original. Except for that it will return paths in leftmost order rather than rightmost. But changing the order of some of those checks will get you back the original rightmost behavior and lazy semantics. Left as an exercise for the OP :-)
Oh, ok! :) I think I got it now! Thank you! Cheers, Paulo Matos
Luke
Later on we noticed that this could be simply written as: findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = []
without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments? 2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments?
Cheers,
-- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Paulo Jorge Matos - pocm at soton.ac.uk http://www.personal.soton.ac.uk/pocm PhD Student @ ECS University of Southampton, UK
participants (21)
-
Aaron Denney
-
Alistair Bayley
-
Andrew Coppin
-
Benja Fallenstein
-
Derek Elkins
-
Henning Thielemann
-
Ian Lynagh
-
Janis Voigtlaender
-
Johan Tibell
-
John Meacham
-
Jules Bean
-
Lennart Augustsson
-
Luke Palmer
-
Neil Mitchell
-
Pablo Nogueira
-
Paulo J. Matos
-
Roberto Zunino
-
Ryan Ingram
-
Stefan O'Rear
-
Tillmann Rendel
-
Yitzchak Gale