<div dir="ltr">On Mon, Apr 29, 2013 at 10:05 AM, Duncan Coutts <span dir="ltr">&lt;<a href="mailto:duncan.coutts@googlemail.com" target="_blank">duncan.coutts@googlemail.com</a>&gt;</span> wrote:<br><div class="gmail_extra">
<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Thu, 2013-04-25 at 00:52 +0200, Gábor Lehel wrote:<br>
&gt; On Wed, Apr 24, 2013 at 7:56 PM, Bryan O&#39;Sullivan &lt;<a href="mailto:bos@serpentine.com">bos@serpentine.com</a>&gt;wrote:<br>
&gt;<br>
&gt; &gt; On Wed, Apr 24, 2013 at 10:47 AM, Duncan Coutts &lt;<br>
&gt; &gt; <a href="mailto:duncan.coutts@googlemail.com">duncan.coutts@googlemail.com</a>&gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt;&gt; I address it briefly in my thesis [1], Section 4.8.2. I think it&#39;s a<br>
&gt; &gt;&gt; fundamental limitation of stream fusion.<br>
&gt; &gt;&gt;<br>
&gt; &gt;<br>
&gt; &gt; See also concat, where the naive fusion-based implementation has quadratic<br>
&gt; &gt; performance:<br>
&gt; &gt;<br>
&gt; &gt; concat :: [Text] -&gt; Text<br>
&gt; &gt; concat txts = unstream (Stream.concat (List.map stream txts))<br>
&gt; &gt;<br>
&gt; &gt; I&#39;ve never figured out how to implement this with sensible characteristics<br>
&gt; &gt; within the fusion framework.<br>
&gt; &gt;<br>
&gt;<br>
&gt; If you could &quot;solve&quot; concat, might that also lead to be being able to do<br>
&gt; without the Skip constructor?<br>
<br>
</div>Dan is right, we still need Skip. My suggested &quot;solution&quot; to the<br>
concatmap problem is also mostly independent of the skip issue.<br>
<br>
You shouldn&#39;t think of skip as being a hack. It&#39;s not. It&#39;s how we<br>
express a more general class of producers in a way that is productive.</blockquote><div><br></div><div style> To further this, note that in a total language, with the type:</div><div style><br></div><div style>    codata Stream a = End | Yield a (Stream a)</div>
<div style><br></div><div style>filter is not definable; it is not a total function. At least, barring an extra proof of some sort that the predicate will yield true after a finite amount of time. concat is similar.</div>
<div style><br></div><div style>Also, adding Skip (Stream a) is a relatively standard way of explicitly representing lazy, partial values. (This is opposed to the partiality monad, which is like an encoding of strict general recursion). That is, if νF is the type of total values, then ν(F + Id) is the type of partial values. I don&#39;t know how easy it is to delete from a more complex tree using just that extension, but in theory you could productively represent arbitrary manipulations with just that, I believe.</div>
</div><br></div><div class="gmail_extra" style>-- Dan</div></div>