[Haskell-cafe] Type systems preventing laziness-related memory leaks?

[Atze van der Ploeg]

I'm not awake yet. That paper is not what you asked at all.

I'm not aware of any paper that presents a type system statically ruling

out thunks of unbounded depth, but it seems to me like this indeed should
be possible.


On Feb 18, 2015 7:24 AM, "Atze van der Ploeg" <atzeus at gmail.com> wrote:

> See the paper "copatterns" by andreas abel.
>
> Cheers!
>
> Atze
> On Feb 18, 2015 6:04 AM, "Eugene Kirpichov" <ekirpichov at gmail.com> wrote:
>
>> Hello haskell-cafe,
>>
>> Let me repost here a question I posted to cstheory stackexchange - in
>> hopes that there are more type theory experts here.
>>
>>
>> http://cstheory.stackexchange.com/questions/29518/type-systems-preventing-laziness-related-memory-leaks
>>
>> 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.
>>
>> Are there any type systems which statically enforce lack of such thunks
>> in a program using a lazy language?
>>
>> 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.
>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150218/984dd605/attachment.html>