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