<p>Levy's <a href="http://requestforlogic.blogspot.co.uk/2011/08/embracing-and-extending-levy-language.html" rel="nofollow">call by push value</a> calculus makes a distinction between values and their thunks.  For a value <code>v</code> of type <code>ty</code> the computation <code>thunk v</code> has type <code>U ty</code>.  Lindley and McBride's <a href="http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-march2014.pdf" rel="nofollow">Frank</a> language, inspired by CBPV, also makes this distinction between computations and values explicit, though unlike Haskell, Frank is strict.</p>

CC BY-SA 3.0
2015-02-18T09:54:53.760Z
2015-02-18T09:54:53.760Z
Dominic Mulligan
<p>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 <code>sum = foldr (+) 0</code> in Haskell.</p>

<p>Are there any type systems which statically enforce lack of such thunks in a program using a lazy language?</p>

<p>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.</p>

<type-theory><functional-programming><program-verification>
Type systems preventing laziness-related memory leaks?
jkff
# Type systems preventing laziness-related memory leaks?

(Asked by: username_0 on 2015-02-17)

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.

**Tags:** type-theory, functional-programming, program-verification


---

## 1 answers

### Answer by username_1 on 2015-02-18. Score: 3

Levy's [call by push value](http://requestforlogic.blogspot.co.uk/2011/08/embracing-and-extending-levy-language.html) calculus makes a distinction between values and their thunks. For a value `v` of type `ty` the computation `thunk v` has type `U ty`. Lindley and McBride's [Frank](http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-march2014.pdf) language, inspired by CBPV, also makes this distinction between computations and values explicit, though unlike Haskell, Frank is strict.


---

