<div dir="ltr"><br><br><div class="gmail_quote">On Tue Feb 17 2015 at 11:50:20 PM Roman Cheplyaka <<a href="mailto:roma@ro-che.info">roma@ro-che.info</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Note that foldr (+) 0 has nothing to do with laziness — it's eager. Its<br>
problem is that it's not tail-recursive.<br></blockquote><div>The problem is that when you say foldr (+) 0 [1, 2, 3, 4, 5] you build a thunk "1 + (2 + (3 + (4 + (5 + 0))))", which has - let's call it "whnf evaluation depth" of 4 (you need a stack of size 4 to evaluate it to whnf).</div><div><br></div><div>I would like a type system that would disallow building thunks with *unbounded* whnf evaluation depth.</div><div><br></div><div>I'm thinking we could annotate every type in every type signature with this depth. Let us use a special kind "@" for these annotations, allow polymorphism on them, and use "t@d" to denote "a value of type t requiring whnf evaluation depth d".</div><div><br></div><div>(+) :: forall (a:@) (b:@) . Int@a -> Int@b -> Int@(1+max(a,b));</div><div><br></div><div>($) :: forall (a:@) (b:@->@) . (forall (a:@) (b:@->@) . x@a -> y@(b a)) -> x@a -> y@(b a)</div><div><br></div><div><span style="font-size:13.1999998092651px">The type signature for (.) quickly gets unwieldy and I wasn't able to even write down the signature for foldr :) but perhaps you get the idea.</span></div><div><span style="font-size:13.1999998092651px"><br></span></div><div><span style="font-size:13.1999998092651px">Some informal properties this would have:</span></div><div><span style="font-size:13.1999998092651px">* whnf depth of calling a function in a tailcall position is max(whnf depth of the function itself, whnf depth of its argument).</span></div><div><span style="font-size:13.1999998092651px">* whnf depth of "case x of { ... }" is 1.</span></div><div><span style="font-size:13.1999998092651px">* In the context of "case x of { ...(primitive pattern)... }", whnf depth of x is 0.</span></div><div><span style="font-size:13.1999998092651px"> </span><br></div><div><span style="font-size:13.1999998092651px">Does this make any sense?</span></div><div><span style="font-size:13.1999998092651px"><br></span></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
foldl (+) 0 would be an example of a laziness issue.<br>
<br>
If you want to specify which functions should or shouldn't be used in a<br>
lazy context, take a look at polarity (see Harper's Practical<br>
Foundations for Programming Languages). So you could say, for instance,<br>
that it doesn't make sense to use + in a lazy context; that'd eliminate<br>
half the cases of laziness-induced memory leaks in practice.<br>
<br>
If instead you want to impose some upper bound on the memory consumption<br>
without caring about specific cases, then see this ICFP'12 paper:<br>
<a href="http://www.dcc.fc.up.pt/~pbv/AALazyExtended.pdf" target="_blank">http://www.dcc.fc.up.pt/~pbv/<u></u>AALazyExtended.pdf</a><br>
<br>
On 18/02/15 07:04, Eugene Kirpichov wrote:<br>
> Hello haskell-cafe,<br>
><br>
> Let me repost here a question I posted to cstheory stackexchange - in<br>
> hopes that there are more type theory experts here.<br>
><br>
> <a href="http://cstheory.stackexchange.com/questions/29518/type-systems-preventing-laziness-related-memory-leaks" target="_blank">http://cstheory.stackexchange.<u></u>com/questions/29518/type-<u></u>systems-preventing-laziness-<u></u>related-memory-leaks</a><br>
><br>
> Perhaps the main source of performance problems in Haskell is when a<br>
> program inadvertently builds up a thunk of unbounded depth - this causes<br>
> both a memory leak and a potential stack overflow when evaluating. The<br>
> classic example is defining sum = foldr (+) 0 in Haskell.<br>
><br>
> Are there any type systems which statically enforce lack of such thunks<br>
> in a program using a lazy language?<br>
><br>
> Seems like this should be on the same order of difficulty as proving<br>
> other static program properties using type system extensions, e.g. some<br>
> flavors of thread safety or memory safety.<br>
<br>
</blockquote></div></div>