This short guide assumes
familiarity with linear types (see the README for resources about linear types
if you are unfamiliar).
- The
Prelude.Linearmodule is a good place to start. It is a prelude for Haskell programs that use-XLinearTypesand is meant to replace the original prelude frombase. - For mutable data with a pure API,
consider looking at
Data.{Array, Hashmap, Vector, Set}.Mutable.Linear. - A linear
IOmonad is inSystem.IO.Linear.- A variant of linear
IOwhich lets you enforce resource safety can be found inSystem.IO.Resource.Linear.
- A variant of linear
- Streams in the style of the
streaminglibrary is inStreaming.LinearandStreaming.Prelude.Linear. - How
Prelude.Linearclasses relate to theirbase(non-linear) counterpart is described in the class comparison table.
There are many other modules of course but a lot of the ones not already listed
are still experimental, such as system-heap memory management in Foreign.Marshall.Pure.
Typically, variants of common Haskell tools and facilities
share the same name with a Linear postfix. For instance,
Data.Bool.Linear provides the linear versions of not
and &&.
The module names follow the typical hierarchical module
naming scheme with top-level names like Control, Data, System
and so on.
Frequently enough, you will want to consume a linear value, or maybe
use it multiple time. The basic tools you need to do this are in
Data.Unrestricted and are typically re-exported by
Prelude.Linear.
Interfacing linear code with regular Haskell is done, for instance, through the type Ur.
The data type Ur, short for unrestricted lets you store an
unrestricted value inside a linear value.
We've designed linear-base to work nicely with the following import conventions:
import qualified Data.Functor.Linear as Dataimport qualified Control.Functor.Linear as Control
Most modules with {-# LANGUAGE LinearHaskell #-} will want to have a mix of
linear and non-linear code and, for example, import linear modules like
Data.Functor.Linear and unrestricted modules from base like Data.List.
The pattern we've followed internally is to import the non-linear module
qualified. For instance:
import Prelude.Linear
import Data.Functor.Linear
import qualified Prelude as NonLinear
import Data.List as ListSometimes it's easier to use forget :: (a %1-> b) -> (a -> b) from
Prelude.Linear than to import the non-linear version of some function.
This is useful in passing linear functions to higher order functions.
For non HOF uses, we can use linear functions directly; given a linear function
f, we can always write g x = f x for g :: A -> B.
This style function is used throughout linear-base, particularly
with mutable data structures.
It serves to limit the scope of using SomeType by taking
a function of type (SomeType %1-> Ur b)
as its second argument and using it with a value of type SomeType to
produce an Ur b. We call this function of type (SomeType %1-> Ur b),
a scope function or just scope for short.
The SomeType cannot escape the scope function by being inside the type b
in some way. This is because the SomeType is bound linearly in the scope
function and Ur can only contain unrestricted (in particular not linear)
values. At any nested level, the SomeType would have to be used in an
unrestricted way.
Now, if f is the only function that can make a SomeType,
then we have an API that completely controls the creation-to-deletion
lifetime (i.e, the scope) of SomeType.
The following will fail to type check:
idBad1 :: a %1-> a
idBad1 x = y
where
y = x
idBad2 :: a %1-> a
idBad2 x = let y = x in yThis is because GHC assumes that anything used in a where-binding or
let-binding is consumed with multiplicity Many. Workaround: inline
these bindings or use sub-functions.
inlined1 :: a %1-> a
inlined1 x = x
useSubfunction :: Array a %1-> Array a
useSubfunction arr = fromRead (read arr 0)
where
fromRead :: (Array a, Ur a) %1-> Array a
fromRead = undefined