Stefan,<div><br></div><div>Thank you for the detailed response! In trying to follow your email I got a bit confused by your notation - </div><div><br></div><div><blockquote class="gmail_quote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; ">
 const :: a -&gt; b -&gt; a </blockquote><blockquote class="gmail_quote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; ">
<span class="Apple-style-span" style="border-collapse: collapse; color: rgb(34, 34, 34); "> const x y = x<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); "> </span></span></blockquote>
<blockquote class="gmail_quote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; ">
<span class="Apple-style-span" style="border-collapse: collapse; color: rgb(34, 34, 34); ">could read<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); "> </span></span></blockquote><blockquote class="gmail_quote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; ">
<span class="Apple-style-span" style="border-collapse: collapse; color: rgb(34, 34, 34); "> a -&gt; {S} -&gt; b -&gt;{L} a</span></blockquote><div> </div><blockquote class="gmail_quote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; ">
<span class="Apple-style-span" style="border-collapse: collapse; color: rgb(34, 34, 34); ">Here, we have annotated the function-space constructor (-&gt;) with information about whether the corresponding function is strict or lazy in its argument. Indeed, const is lazy in its first argument and lazy in its second.</span></blockquote>
</div><div><br></div><div>Did you mean to say that const is <b>strict </b>in its first param and lazy in its second (since const _|_ y = _|_)? Also, can you explain your notation, how does <span class="Apple-style-span" style="border-collapse: collapse; color: rgb(34, 34, 34); ">a -&gt; {S} -&gt; b -&gt;{L} a indicate the strictness? Why not just {S} a -&gt; {L} b -&gt; a? </span></div>
<div><font class="Apple-style-span" color="#222222"><span class="Apple-style-span" style="border-collapse: collapse;"><br></span></font></div><div><font class="Apple-style-span" color="#222222"><span class="Apple-style-span" style="border-collapse: collapse;">Best,</span></font></div>
<div><font class="Apple-style-span" color="#222222"><span class="Apple-style-span" style="border-collapse: collapse;">Paul<br></span></font><br><div class="gmail_quote">On Wed, Jun 17, 2009 at 6:31 AM, Stefan Holdermans <span dir="ltr">&lt;<a href="mailto:stefan@cs.uu.nl">stefan@cs.uu.nl</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Dear Paul,<br>
<br>
This thread as well as your blog post is very interesting. Hopefully I can add something more or less valuable to it.<br>
<br>
On your blog, you mention that your scheme for run-time strictness analysis doesn&#39;t work out because it&#39;ll have you force a function first before you can find out about its strictness. I guess this can be easily overcome by separating the function from the strictness information it carries.<br>

<br>
One way to do this, would be by storing strictness information in the type of a function. Actually, this is exactly what type-based approaches to strictness analyses do. So, for example, an extended type of the function const,<br>

<br>
  const :: a -&gt; b -&gt; a<br>
  const x y = x<br>
<br>
could read<br>
<br>
  a -&gt; {S} -&gt; b -&gt;{L} a<br>
<br>
Here, we have annotated the function-space constructor (-&gt;) with information about whether the corresponding function is strict or lazy in its argument. Indeed, const is lazy in its first argument and lazy in its second. (Note that this is very simple take on storing strictness information in types: there is plenty more to say about it, but I will refrain from that.)<br>

<br>
An annotated type like the one above can be easily inferred by a strictness analyser. But what exactly is type inference? Well, one way to look at it is a means to reconstruct typing information that was left out from the program. For example, if we infer the type a -&gt; b -&gt; a for the const function in Haskell, we are effectively completing the definition of const with explicit type information. This information can then be stored in the program. Using Java-like syntax:<br>

<br>
  const &lt;a&gt; &lt;b&gt; (x :: a) (y :: b) = x<br>
<br>
So, now const takes two extra arguments, both of which are types rather than values. When, calling a polymorphic function, type inference then computes the type arguments for a specific instantiation of the polymorphic function:<br>

<br>
  const 2 &#39;x&#39;<br>
<br>
becomes<br>
<br>
  const &lt;Int&gt; &lt;Char&gt; 2 &#39;x&#39;<br>
<br>
While typing information can proof valuable to have around at compile type, we don&#39;t actually want types to be passed around at run time. Luckily, in Haskell no run-time decisions can be made based on these type arguments, so all these extra abstractions and applications can be erased when generating code for a program.<br>

<br>
Pretty much the same holds for the strictness annotations that are inferred by a strictness analyser. Inferring strictness can be thought of as decorating the program. For instance, for const we get something like:<br>
<br>
  const &lt;a&gt; &lt;b&gt; (x :: a{S}) (y :: b{L}) = x<br>
<br>
where a {S} indicates strictness and {L} laziness.<br>
<br>
Viewing strictness annotations as types, a natural step is to allow functions to be polymorphic in their strictness annotations as well. This is especially useful for higher-order functions. The function apply, for example,<br>

<br>
  apply :: (a -&gt; b) -&gt; a -&gt; b<br>
  apply f x = f x<br>
<br>
is supposed to work on both strict and lazy functions.  Moreover, depending on whether we pass it a strict or a lazy function as its first argument, it becomes, respectively, strict or lazy in its second argument. This insight can be captured quite nicely by means of a type that is polymorphic in its strictness annotations:<br>

<br>
  (a -&gt;{i} b) -&gt;{S} -&gt;{i} b<br>
<br>
Here, i is a strictness variable that is to be instantiated with either S or L. Decorating the definition of apply may now yield something like<br>
<br>
  apply &lt;a&gt; &lt;b&gt; {i} (f :: (a -&gt;{i} b){S}) (x :: a{i})<br>
<br>
Of course, just as with ordinary types, strictness annotations don&#39;t have to be passed around at run-time: they can be erased from the program and all that are made based on strictness information can then be made at compile time.<br>

<br>
But what if we don&#39;t erase these annotations? Then we can use strictness information to participate in run-time decisions as well---just as you proposed. Let&#39;s explore that idea.<br>
<br>
Performing strictness analysis on foldl,<br>
<br>
  foldl :: (b -&gt; a -&gt; b) -&gt; b -&gt; [a] -&gt; b<br>
  foldl f e []       = e<br>
  foldl f e (x : xs) = foldl f (f e x) xs<br>
<br>
we find the annotated type<br>
<br>
  (b -&gt;{i} -&gt;{j} b) -&gt;{L} b -&gt;{i} [a] -&gt;{S} -&gt; b<br>
<br>
Indeed, whether foldl is strict in its second argument depends on wether its first argument is strict in its own first argument. Let&#39;s decorate the definition of foldl accordingly:<br>
<br>
  foldl &lt;a&gt; &lt;b&gt; {i} {j} (f :: (b -&gt;{i} -&gt;{j} b){L}) (e :: b{i}) (l :: [a]{S}) =<br>
    case l of<br>
      []     -&gt; e<br>
      x : xs -&gt; foldl &lt;a&gt; &lt;b&gt; {i} {j} f (f e x) xs<br>
<br>
Allright, that&#39;s messy, but bear with me. (At this point, we could erase the type arguments and only keep the strictness arguments for we only want the latter to play a role at run time, but let&#39;s keep them both, just to be uniform.)<br>

<br>
Now, let&#39;s apply the foldl to (+), 0, and [1 .. 1000000] assuming that (+) is strict in both its arguments and specialised to Int,<br>
<br>
  (+) :: Int -&gt;{S} Int -&gt;{S} Int<br>
<br>
and let&#39;s pass in the arguments in three steps. First we pass in the type arguments:<br>
<br>
  foldl &lt;Int&gt; &lt;Int&gt; :: (Int -&gt;{i} Int -&gt;{j} Int) -&gt;{L} Int -&gt;{i} [Int] -&gt;{S} Int<br>
<br>
Then the strictness arguments:<br>
<br>
  foldl &lt;Int&gt; &lt;Int&gt; &lt;S&gt; &lt;S&gt; :: (Int -&gt;{S} -&gt;Int -&gt;{S} Int) -&gt;{L} Int -&gt;{S} [Int] -&gt;{S} Int<br>
<br>
Now we have obtained a specialised version of foldl that is lazy in its first argument and strict in its second and third argument! When passing in the remaining three arguments we can thus indeed evaluate the second argument before we pass it to foldl:<br>

<br>
  foldl &lt;Int&gt; &lt;Int&gt; &lt;S&gt; &lt;S&gt; (+) (0) [1 .. 1000000]<br>
<br>
Moreover, this can be done for each recursive call as well, effectively having the computation require constant space.<br>
<br>
So, the on strictness information depending decision that is to made here, is to apply functions strictly or lazily. Funnily, if we are willing to do the static part of the strictness analysis by hand, we can already experiment a bit with this scheme in Haskell. (I&#39;ve attached the source code.)<br>

<br>
First, let us abstract from function types annotated with S or L and introduce a type class:<br>
<br>
  infixl 9 #<br>
<br>
  class Fun f where<br>
    lam :: (a -&gt; b) -&gt; f a b<br>
    (#) :: f a b -&gt; (a -&gt; b)<br>
<br>
That is, functions are constructed by means of the method lam and applied (destructed) by means of (#).<br>
<br>
Haskell&#39;s built-in lazy function space (-&gt;) provides a natural implementation of the class:<br>
<br>
  instance Fun (-&gt;) where<br>
    lam = id<br>
    (#) = ($)<br>
<br>
In addition, we provide a strict function-space constructor (:-&gt;):<br>
<br>
  newtype a :-&gt; b = S {unS :: a -&gt; b}<br>
<br>
  instance Fun (:-&gt;) where<br>
    lam = S<br>
    (#) = \f x -&gt; unS f $! x<br>
<br>
Now we can have a &quot;hand-annotated&quot; version of foldl:<br>
<br>
  foldl :: (Fun i, Fun j) =&gt; i b (j a b) -&gt; i b ([a] :-&gt; b)<br>
  foldl = lam $ \f -&gt; lam $ \e -&gt; lam $ \l -&gt; case l of<br>
            []     -&gt; e<br>
            x : xs -&gt; foldl # f # (f # e # x) # xs<br>
<br>
Note how the type arguments i and j play the roles of the strictness annotations from the explanation above. Furthermore we have replaced Haskell&#39;s lambda abstraction by means of abstraction through lam and Haskell&#39;s function application by application through (#). Apart from that, this is just your ordinary foldl. Well... :-)<br>

<br>
What&#39;s important to note is that the transformation from the &quot;normal&quot; definition of foldl to this annotated beast could be performed at compile time by a strictness analyser.<br>
<br>
Now, let&#39;s try it out. Say we have two versions of addition on integers: a lazy one (lplus) and a strict one (splus). Note the types:<br>
<br>
  lplus :: Int -&gt; Int -&gt; Int<br>
  lplus = (+)<br>
<br>
  splus :: Int :-&gt; Int :-&gt; Int<br>
  splus = lam $ \m -&gt; lam $ \n -&gt; ((+) $! m) $! n<br>
<br>
There we go:<br>
<br>
  *Main&gt; foldl # lplus # 0 # [1 .. 1000000]<br>
  *** Exception: stack overflow<br>
<br>
  *Main&gt; foldl # splus # 0 # [1 .. 1000000]<br>
  1784293664<br>
<br>
Isn&#39;t that neat?<br>
<br>
Of course, whether this scheme would work out in practice depends on whether the cost of lazy evaluation really outweighs the cost of passing around strictness information. I&#39;m not so sure, but I would be interested to see the results of experiments with this idea. An important factor seems to be how much strictness information that is passed around in a naive implementation of this scheme can be eliminated by &quot;normal&quot; compiler optimisations.<br>

<br>
Well, just my two cents. :-)<br>
<br>
Cheers,<br><font color="#888888">
<br>
  Stefan<br>
<br>
</font><br><br>
<br></blockquote></div><br></div>