... | ... | @@ -88,3 +88,97 @@ There is however an improvement to be had on top of the simple strategy. Namely, |
|
|
|
|
|
|
|
|
A consequence of this choice is that linear data will only exist when pointed to by non-linear data structures.
|
|
|
|
|
|
# Controlling sharing (full laziness)
|
|
|
|
|
|
|
|
|
According to de Vries
|
|
|
([ http://www.well-typed.com/blog/2016/09/sharing-conduit/](http://www.well-typed.com/blog/2016/09/sharing-conduit/)):
|
|
|
|
|
|
>
|
|
|
> \[...\] In the presence of the full laziness optimization we have no
|
|
|
> control over when values are not shared. While it is possible in
|
|
|
> theory to write code in such a way that the lazy data structures are
|
|
|
> self-referential and hence keeping them in memory does not cause a
|
|
|
> memory leak, in practice the resulting code is too brittle and writing
|
|
|
> code like this is just too difficult.
|
|
|
|
|
|
>
|
|
|
> \[...\]
|
|
|
|
|
|
>
|
|
|
> Full laziness can be disabled using `-fno-full-laziness`, but sadly this
|
|
|
> throws out the baby with the bathwater. In many cases, full laziness
|
|
|
> is a useful optimization.
|
|
|
|
|
|
|
|
|
Linearity offers a solution to the problem. Indeed, linearly-typed
|
|
|
values are used once only. Thus, linearity implies that no sharing is
|
|
|
intended by the programmer. In turn, the full laziness optimization
|
|
|
cannot apply to expressions in a linear context.
|
|
|
|
|
|
|
|
|
Consider now a simple example which exhibits the problem, also provided
|
|
|
by de Vries:
|
|
|
|
|
|
```
|
|
|
ni_mapM_::(a ->IO b)->[a]->IO(){-# NOINLINE ni_mapM_ #-}ni_mapM_= mapM_
|
|
|
|
|
|
main2::IO()main2= forM_ [1..5]$\_-> ni_mapM_ print [1..N]
|
|
|
```
|
|
|
|
|
|
|
|
|
One would expect that the above programs uses constant space (because
|
|
|
the list `[1..N]` is produced lazily). However, if one compiles the
|
|
|
above program with full laziness and runs it, one observes a memory
|
|
|
residency proportional to N. This happens because GHC shares the
|
|
|
intermediate list `[1..N]` between runs of `ni_mapM_ print [1 .. N]`.
|
|
|
|
|
|
|
|
|
Let us now consider an equivalent program, be written using our
|
|
|
proposed extension for linear types. (To transpose the example with
|
|
|
minimal changes we have to redefine several basic types and functions
|
|
|
--- in a practical application this would not happen because we would
|
|
|
actually be using a custom streaming library, as de Vries does).
|
|
|
|
|
|
```
|
|
|
data[a]where[]::[a](:):: a ⊸[a]⊸[a]discard::Int⊸IO()ni_mapM_::(a ⊸IO b)→List a ⊸IO()forM_::List a ⊸(a ⊸IO())→IO()main2::1IO()main2= forM_ [1..5]$\i ->do
|
|
|
discard i
|
|
|
ni_mapM_ print [1..N]
|
|
|
```
|
|
|
|
|
|
|
|
|
In the above example, it is incorrect to share the intermediate
|
|
|
list. Indeed, performing full laziness would amount to transform the
|
|
|
program into the following form, which is not well-typed:
|
|
|
|
|
|
```
|
|
|
main2::1IO()main2=let xs ::1[a]
|
|
|
xs =[1..N]in forM_ [1..5]$\i ->do
|
|
|
discard i
|
|
|
ni_mapM_ print xs
|
|
|
```
|
|
|
|
|
|
|
|
|
Indeed, the above definition attempts to use `xs` several times, while
|
|
|
it is bound only once.
|
|
|
|
|
|
|
|
|
In our proposed extension, one could still write the following
|
|
|
type-correct program, which introduces explicit sharing:
|
|
|
|
|
|
```
|
|
|
main2::1IO()main2=let xs ::ω [a]
|
|
|
xs =[1..N]in forM_ [1..5]$\i ->do
|
|
|
discard i
|
|
|
ni_mapM_ print xs
|
|
|
```
|
|
|
|
|
|
|
|
|
Yet, thanks to linearity annotations, the programmer intentionally
|
|
|
marked the expressions which are not supposed to be shared, in effect
|
|
|
precisely controlling where (not) to apply full-laziness. Moreover,
|
|
|
the user of a library written for streams would never have to worry
|
|
|
about inadvertent sharing, because the types of the library functions
|
|
|
would specify exactly the right behavior.
|
|
|
See [ https://jyp.github.io/pdf/Organ.pdf](https://jyp.github.io/pdf/Organ.pdf) for how such a library may look like. |