[Haskell-cafe] Type systems preventing laziness-related memory leaks?
roma at ro-che.info
Wed Feb 18 07:50:17 UTC 2015
Note that foldr (+) 0 has nothing to do with laziness — it's eager. Its
problem is that it's not tail-recursive.
foldl (+) 0 would be an example of a laziness issue.
If you want to specify which functions should or shouldn't be used in a
lazy context, take a look at polarity (see Harper's Practical
Foundations for Programming Languages). So you could say, for instance,
that it doesn't make sense to use + in a lazy context; that'd eliminate
half the cases of laziness-induced memory leaks in practice.
If instead you want to impose some upper bound on the memory consumption
without caring about specific cases, then see this ICFP'12 paper:
On 18/02/15 07:04, Eugene Kirpichov 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.
> 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.
More information about the Haskell-Cafe