I don&#39;t even understand what your notation means.<br><br>But apart from that, there are good reasons to define strictness denotationally instead of operationally.&nbsp; 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>&nbsp; -- Lennart<br><br><div class="gmail_quote">On Dec 4, 2007 11:07 PM, Ryan Ingram &lt;<a href="mailto:ryani.spam@gmail.com">
ryani.spam@gmail.com</a>&gt; 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>&gt; f _|_ = _|_</div>
<div>&nbsp;</div>
<div>instead of, for example,</div>
<div>&gt; forall x :: Exception. f (throw x) = throw x</div>
<div>where&nbsp;an exception thrown from pure code is observable in IO.<br>&nbsp;</div>
<div>In the second case we need to prove that the argument is evaluated at some point, which is&nbsp;also equivalent to the halting problem but more captures the notion of &quot;f evaluates its argument&quot; rather than &quot;either f evaluates its argument, or&nbsp;f _ is _|_&quot;
</div>
<div>&nbsp;</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>&nbsp;</div>
<div>&nbsp; -- ryan<br>&nbsp;</div>
<div><div><div></div><div class="Wj3C7c"><span class="gmail_quote">On 12/4/07, <b class="gmail_sendername">Stefan O&#39;Rear</b> &lt;<a href="mailto:stefanor@cox.net" target="_blank">stefanor@cox.net</a>&gt; 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>&gt; Hello all,<br>&gt;<br>&gt; As you might have possibly read in some previous blog posts:
<br>&gt; <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>&gt; <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>&gt;<br>&gt; we (the FPSIG group) defined:<br>&gt; data BTree a = Leaf a<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| Branch (BTree a) a (BTree a)<br>&gt;<br>&gt; and a function that returns a list of all the paths (which are lists
<br>&gt; of node values) where each path element makes the predicate true.<br>&gt; findAllPath :: (a -&gt; Bool) -&gt; (BTree a) -&gt; Maybe [[a]]<br>&gt; findAllPath pred (Leaf l) | pred l = Just [[l]]<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; | otherwise = Nothing
<br>&gt; findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath pred lf<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;rtpaths = findAllPath pred rt<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in
<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if isNothing lfpaths &amp;&amp;<br>&gt; isNothing rtpaths<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;then Nothing<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;else
<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if isNothing lfpaths<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;then Just (map (r:)<br>&gt; $ fromJust rtpaths)<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;else
<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if isNothing rtpaths<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;then Just (map<br>&gt; (r:) $ fromJust lfpaths)<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;else Just (map
<br>&gt; (r:) $ fromJust rtpaths ++ fromJust lfpaths)<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; | otherwise = Nothing<br>&gt;<br>&gt; Later on we noticed that this could be simply written as:<br>&gt; findAllPath :: (a -&gt; Bool) -&gt; (BTree a) -&gt; [[a]]
<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; findAllPath pred = g where<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; g (Leaf l) | pred l = [[l]]<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred<br>&gt; lf) ++ (findAllPath pred rt)<br>&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; g _&nbsp;&nbsp;= []
<br>&gt;<br>&gt; without even using maybe. However, 2 questions remained:<br>&gt; 1 - why is the first version strict in its arguments?<br><br>Because of the definition of strictness.&nbsp;&nbsp;A function is strict iff f<br>undefined = undefined.
<br><br>findAllPath pred undefined -&gt; undefined because of the case analysis<br>findAllPath undefined (Leaf _) -&gt; undefined because pred is applied in<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; the guard<br>findAllPath undefined Branch{} -&gt; undefined because pred is applied in
<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; the guard<br><br>&gt; 2 - if it really is strict in its arguments, is there any automated<br>&gt; 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 &lt;- [1,3.], i == sum [ k | k &lt;- [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.&nbsp;&nbsp;(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>