<div dir="ltr"><div>Hello haskell-cafe,</div><div><br></div><div>Let me repost here a question I posted to cstheory stackexchange - in hopes that there are more type theory experts here.</div><div><br></div><a href="http://cstheory.stackexchange.com/questions/29518/type-systems-preventing-laziness-related-memory-leaks">http://cstheory.stackexchange.com/questions/29518/type-systems-preventing-laziness-related-memory-leaks</a><br><div><br></div><div><div>Perhaps the main source of performance problems in Haskell is when a program inadvertently builds up a thunk of unbounded depth - this causes both a memory leak and a potential stack overflow when evaluating. The classic example is defining sum = foldr (+) 0 in Haskell.</div><div><br></div><div>Are there any type systems which statically enforce lack of such thunks in a program using a lazy language?</div><div><br></div><div>Seems like this should be on the same order of difficulty as proving other static program properties using type system extensions, e.g. some flavors of thread safety or memory safety.</div><div><br></div></div></div>