wiki:LinearTypes/Examples

Examples of programs benefiting from linear types fall into three categories.

Enforcement of protocol

Linear types can be used to encode protocols, in a way very similar to 'session types'. Linearity checks ensure that the protocol is respected (so one does not backtrack or drops out).

type a  b = ... {- see proposal -}
type a  b = ... {- see proposal -}
type Effect = IO () -- for example

pr :: Double -> Effect -- "prints" a number

type N a = a  Effect

data Client
  = Mul Double Double (N (Double  Server)) -- Client sends two 'Double' and
                                            -- expects a double and a new server
                                            -- session.
  | Terminate
type Server = N Client


exampleClient :: N (N Client)
exampleClient server = server $ Mul 12 34 $ \(product,server') ->
  -- do something with the product
  pr product >> server' Terminate

exampleServer :: Server
exampleServer client = case client of
  Mul x y k -> k (x*y,exampleServer)
  Terminate -> return ()

Correctness of optimized code

Writing programs in the polarized style shown above is very useful to write efficient programs.

In general, fusion in GHC relies on the rewrite rules and the inliner.

  1. Rewrite rules transform code using general recursion into a representation with no recursion (eg. church encodings)
  2. The inliner kicks in and 'fuses' composition of non-recursive functions
  3. Unfused code may be reverted to the original representation.

The problem with this scheme is that it involves two phases of heuristics (rules and inliner), and in practice programmers have difficulties to predict the performance of any given program.

A partial remedy to this solution is to stop relying on rewrite rules, and use directly non-recursive representations. For example the following representation from Lippmeier et al. http://benl.ouroborus.net/papers/2016-polarized/dpdf-FHPC2016-preprint.pdf:

data Sources i m e = Sources -- 'i' is the array's index type, 'e' the type of elements and 'm' the effects
  { arity :: i
  , pull  :: i -> (e -> m ()) -> m () -> m () } -- 'pull' is an iterator to apply to every elements of the array (like 'traverse')

data Sinks i m e = Sinks
  { arity :: i
  , push  :: i -> e -> m ()
  , eject :: i -> m () }

Such representations are typically functionals, and thus do not consume memory. One eventually gets code which is guaranteed to be 'fused'. For instance, in the following example from Lippmeier et al., neither the source nor the sink represent data in memory.

copySetP :: [FilePath] -> [FilePath] -> IO ()
copySetP srcs dsts = do
  ss <- sourceFs srcs
  sk <- sinkFs   dsts
  drainP ss sk

One then faces two classes of new problems.

First, any non-linear (precisely non-affine) use of such a representation will duplicate work. For example:

example srcs dsts = do
  ss <- expensiveComputation <$> sourceFs srcs
  sk <- sinkFs  dsts
  drainP ss sk
  drainP ss sk -- expensiveComputation is run a second time here.

If one is not careful, one may end up with a program which does not use any intermediate memory, but duplicates a lot of intermediate computations. Linear types solve the problem by preventing such duplications. (Combinators may be still provided to duplicate computation explicitly or store intermediate results explicitly.)

Second, such representations may contain effects. In this situation, non-linear uses may produce an incorrect program. If one takes the example of a non-recursive representation of files, one may have two processes writing simultaneously in the same file (potentially corrupting data), or one may forget to close the file.

Quoting Lippmeier et al.:

In general an object of type Sources is an abstract producer of data, and it may not even be possible to rewind it to a previous state — suppose it was connected to a stream of sensor readings. Alas the Haskell type system does not check linearity so we rely on the programmer to enforce it manually.

Literature on this style of non-recursive representations includes additionally:

Diminishing GC pressure

Because linear values cannot be shared, they should in principle not be subject to GC. Indeed, the consumer of the value (pattern matching) may very well perform de-allocation of the spot. Thus linear values can be stored in a heap outside of GC control. Alone, this strategy will diminish GC usage, but may increase the total running time of the program (if only because allocation in the GC heap is so efficient that it beats manual memory management for short-lived object) [Wakeling and Runciman have experienced this effect]. Yet, the tradeoff may be worth the trouble if long-tail in latencies is a bigger problem than absolute runtime.

There is however an improvement to be had on top of the simple strategy. Namely, to always fuse composition of linear functions. This strategy removes many short-lived objects. Fusing always is safe performance wise thanks to linearity. It is a good idea because it allows the programmer to predict accurately the behavior of the generated code.

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/):

[...] 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 ::1 IO ()
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 ::1 IO ()
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 ::1 IO ()
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 for how such a library may look like.

Last modified 14 months ago Last modified on Sep 30, 2016 10:51:45 AM