Changes between Version 4 and Version 5 of LinearTypes/Examples


Ignore:
Timestamp:
Sep 30, 2016 10:51:45 AM (3 years ago)
Author:
jpbernardy
Comment:

Full laziness issue.

Legend:

Unmodified
Added
Removed
Modified
  • LinearTypes/Examples

    v4 v5  
    9999A consequence of this choice is that linear data will only exist when pointed to by non-linear data structures.
    100100
     101= Controlling sharing (full laziness) =
     102
     103According to de Vries
     104(http://www.well-typed.com/blog/2016/09/sharing-conduit/):
     105
     106
     107  [...] In the presence of the full laziness optimization we have no
     108  control over when values are not shared. While it is possible in
     109  theory to write code in such a way that the lazy data structures are
     110  self-referential and hence keeping them in memory does not cause a
     111  memory leak, in practice the resulting code is too brittle and writing
     112  code like this is just too difficult.
     113
     114  [...]
     115
     116  Full laziness can be disabled using `-fno-full-laziness`, but sadly this
     117  throws out the baby with the bathwater. In many cases, full laziness
     118  is a useful optimization.
     119
     120
     121Linearity offers a solution to the problem. Indeed, linearly-typed
     122values are used once only. Thus, linearity implies that no sharing is
     123intended by the programmer. In turn, the full laziness optimization
     124cannot apply to expressions in a linear context.
     125
     126Consider now a simple example which exhibits the problem, also provided
     127by de Vries:
     128
     129{{{#!hs
     130ni_mapM_ :: (a -> IO b) -> [a] -> IO ()
     131{-# NOINLINE ni_mapM_ #-}
     132ni_mapM_ = mapM_
     133
     134main2 :: IO ()
     135main2 = forM_ [1..5] $ \_ -> ni_mapM_ print [1 .. N]
     136}}}
     137
     138One would expect that the above programs uses constant space (because
     139the list `[1..N]` is produced lazily).  However, if one compiles the
     140above program with full laziness and runs it, one observes a memory
     141residency proportional to N. This happens because GHC shares the
     142intermediate list `[1..N]` between runs of `ni_mapM_ print [1 .. N]`.
     143
     144Let us now consider an equivalent program, be written using our
     145proposed extension for linear types. (To transpose the example with
     146minimal changes we have to redefine several basic types and functions
     147--- in a practical application this would not happen because we would
     148actually be using a custom streaming library, as de Vries does).
     149
     150
     151{{{#!hs
     152data [a] where
     153  [] :: [a]
     154  (:) :: a ⊸ [a] ⊸ [a]
     155
     156discard :: Int ⊸ IO ()
     157
     158ni_mapM_ :: (a ⊸ IO b) → List a ⊸ IO ()
     159forM_ :: List a ⊸ (a ⊸ IO ()) → IO ()
     160
     161main2 ::1 IO ()
     162main2 = forM_ [1..5] $ \i -> do
     163  discard i
     164  ni_mapM_ print [1 .. N]
     165}}}
     166
     167In the above example, it is incorrect to share the intermediate
     168list. Indeed, performing full laziness would amount to transform the
     169program into the following form, which is not well-typed:
     170
     171{{{#!hs
     172main2 ::1 IO ()
     173main2 =
     174  let xs ::1 [a]
     175      xs = [1 .. N]
     176  in forM_ [1..5] $ \i -> do
     177       discard i
     178       ni_mapM_ print xs
     179}}}
     180
     181Indeed, the above definition attempts to use `xs` several times, while
     182it is bound only once.
     183
     184In our proposed extension, one could still write the following
     185type-correct program, which introduces explicit sharing:
     186
     187{{{#!hs
     188main2 ::1 IO ()
     189main2 =
     190  let xs ::ω [a]
     191      xs = [1 .. N]
     192  in forM_ [1..5] $ \i -> do
     193       discard i
     194       ni_mapM_ print xs
     195}}}
     196
     197Yet, thanks to linearity annotations, the programmer intentionally
     198marked the expressions which are not supposed to be shared, in effect
     199precisely controlling where (not) to apply full-laziness. Moreover,
     200the user of a library written for streams would never have to worry
     201about inadvertent sharing, because the types of the library functions
     202would specify exactly the right behavior.
     203See https://jyp.github.io/pdf/Organ.pdf for how such a library may look like.
     204