Re: [Haskell-cafe] Why is this strict in its arguments?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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*... ;-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Dec 6, 2007 9:30 AM, Alistair Bayley [EMAIL PROTECTED] wrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On 12/6/07, Luke Palmer [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On 12/6/07, Ryan Ingram [EMAIL PROTECTED] wrote: On 12/6/07, Luke Palmer [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
OK, last post. I clearly need more sleep. On 12/6/07, Ryan Ingram [EMAIL PROTECTED] wrote: mergeMaybes f x y = liftM2 f `mplus` x `mplus` y mergeMaybes f x y = liftM2 f x y `mplus` x `mplus` y ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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
Re: [Haskell-cafe] Why is this strict in its arguments?
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... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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...) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Dec 5, 2007 1:51 PM, Luke Palmer [EMAIL PROTECTED] wrote: On Dec 4, 2007 9:41 PM, Paulo J. Matos [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Dec 5, 2007 11:56 AM, Andrew Coppin [EMAIL PROTECTED] 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. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Dec 5, 2007 12:30 PM, Andrew Coppin [EMAIL PROTECTED] wrote: Luke Palmer wrote: On Dec 5, 2007 11:56 AM, Andrew Coppin [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
Luke Palmer wrote: On Dec 5, 2007 11:56 AM, Andrew Coppin [EMAIL PROTECTED] 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? ;-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Dec 5, 2007 11:44 AM, Jules Bean [EMAIL PROTECTED] wrote: 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. That's a nice little insight. I'll remember that. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Dec 4, 2007 10:00 PM, Neil Mitchell [EMAIL PROTECTED] wrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Dec 5, 2007 10:44 AM, Jules Bean [EMAIL PROTECTED] wrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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. ;-) Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Tue, Dec 04, 2007 at 09:41:36PM +, 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
signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 [EMAIL PROTECTED] wrote:
On Tue, Dec 04, 2007 at 09:41:36PM +, 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
-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
Re: [Haskell-cafe] Why is this strict in its arguments?
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 signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On 12/4/07, Stefan O'Rear [EMAIL PROTECTED] 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. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
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 [EMAIL PROTECTED] 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?
-- ryan
On 12/4/07, Stefan O'Rear [EMAIL PROTECTED] wrote:
On Tue, Dec 04, 2007 at 09:41:36PM +, 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
-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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Tue, Dec 04, 2007 at 03:35:28PM -0800, Ryan Ingram wrote: On 12/4/07, Stefan O'Rear [EMAIL PROTECTED] 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 signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Tue, Dec 04, 2007 at 03:35:28PM -0800, Ryan Ingram wrote: On 12/4/07, Stefan O'Rear [EMAIL PROTECTED] 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⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On 12/4/07, Stefan O'Rear [EMAIL PROTECTED] 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. Your ifac example makes perfect sense, thanks. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
On Tue, Dec 04, 2007 at 07:43:36PM -0800, Ryan Ingram wrote:
On 12/4/07, Stefan O'Rear [EMAIL PROTECTED] 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
signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
