| 101 | = Controlling sharing (full laziness) = |
| 102 | |
| 103 | According 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 | |
| 121 | Linearity offers a solution to the problem. Indeed, linearly-typed |
| 122 | values are used once only. Thus, linearity implies that no sharing is |
| 123 | intended by the programmer. In turn, the full laziness optimization |
| 124 | cannot apply to expressions in a linear context. |
| 125 | |
| 126 | Consider now a simple example which exhibits the problem, also provided |
| 127 | by de Vries: |
| 128 | |
| 129 | {{{#!hs |
| 130 | ni_mapM_ :: (a -> IO b) -> [a] -> IO () |
| 131 | {-# NOINLINE ni_mapM_ #-} |
| 132 | ni_mapM_ = mapM_ |
| 133 | |
| 134 | main2 :: IO () |
| 135 | main2 = forM_ [1..5] $ \_ -> ni_mapM_ print [1 .. N] |
| 136 | }}} |
| 137 | |
| 138 | One would expect that the above programs uses constant space (because |
| 139 | the list `[1..N]` is produced lazily). However, if one compiles the |
| 140 | above program with full laziness and runs it, one observes a memory |
| 141 | residency proportional to N. This happens because GHC shares the |
| 142 | intermediate list `[1..N]` between runs of `ni_mapM_ print [1 .. N]`. |
| 143 | |
| 144 | Let us now consider an equivalent program, be written using our |
| 145 | proposed extension for linear types. (To transpose the example with |
| 146 | minimal changes we have to redefine several basic types and functions |
| 147 | --- in a practical application this would not happen because we would |
| 148 | actually be using a custom streaming library, as de Vries does). |
| 149 | |
| 150 | |
| 151 | {{{#!hs |
| 152 | data [a] where |
| 153 | [] :: [a] |
| 154 | (:) :: a ⊸ [a] ⊸ [a] |
| 155 | |
| 156 | discard :: Int ⊸ IO () |
| 157 | |
| 158 | ni_mapM_ :: (a ⊸ IO b) → List a ⊸ IO () |
| 159 | forM_ :: List a ⊸ (a ⊸ IO ()) → IO () |
| 160 | |
| 161 | main2 ::1 IO () |
| 162 | main2 = forM_ [1..5] $ \i -> do |
| 163 | discard i |
| 164 | ni_mapM_ print [1 .. N] |
| 165 | }}} |
| 166 | |
| 167 | In the above example, it is incorrect to share the intermediate |
| 168 | list. Indeed, performing full laziness would amount to transform the |
| 169 | program into the following form, which is not well-typed: |
| 170 | |
| 171 | {{{#!hs |
| 172 | main2 ::1 IO () |
| 173 | main2 = |
| 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 | |
| 181 | Indeed, the above definition attempts to use `xs` several times, while |
| 182 | it is bound only once. |
| 183 | |
| 184 | In our proposed extension, one could still write the following |
| 185 | type-correct program, which introduces explicit sharing: |
| 186 | |
| 187 | {{{#!hs |
| 188 | main2 ::1 IO () |
| 189 | main2 = |
| 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 | |
| 197 | Yet, thanks to linearity annotations, the programmer intentionally |
| 198 | marked the expressions which are not supposed to be shared, in effect |
| 199 | precisely controlling where (not) to apply full-laziness. Moreover, |
| 200 | the user of a library written for streams would never have to worry |
| 201 | about inadvertent sharing, because the types of the library functions |
| 202 | would specify exactly the right behavior. |
| 203 | See https://jyp.github.io/pdf/Organ.pdf for how such a library may look like. |
| 204 | |