Linear types is closely related to linear logic, where the idea of value consumption is introduced, meaning a value is only valid for one use. In the 90’s, this was found a neat way to represent finite resources which is very interesting for programming languages; this viewpoint is well explained here.
In practice, this whole idea builds on the rule a value of a linear type has to be used exactly once:
This consumption requirement is explicitly indicated with a linear function arrow:
⊸, also called lollipop. This is also what is used in the Tweag I/O GHC fork, which extends the type system to check for correct multiplicity when such arrows are used, in a backward compatible way. In my bachelor thesis we weren’t as clever and split the type universe into linear and non-linear counterparts and did checks this way, which made it much more difficult to use in practice since we couldn’t write functions compatible with both.
What do we gain?
This is actually all there is to it in the practical sense, but this simple concept has very nice consequences. Most of all, it creates a resource aware type system, which not only knows types of values but also number of uses; a linearly typed value is guaranteed to only have one reference to it at any time, duplication or ignoring will not compile.
For example, let’s imagine that we want to model arrays, including an update function:
since we do not know if there are other references to this array when we update it, we need to allocate fresh memory for this updated version. However, if we instead type it as
and only allow linear operations on the arrays, the type system guarantees us that there is only one reference to the incoming array, this one! That means we could implement destructive updates (change the allocated memory in-place) safely, which is splendid since it is both faster and does not require garbage collection since there is always only one reference to the array.
Relevance to streams
With effectful streams (which here refers to the streaming library), the stream elements perform effects in some monad, and access to old stream states can result in really wonky behaviour. Consider this example:
Yikes! The point of a strong type system is to get rid of pesky runtime errors, but the streaming library makes it possible (even though we can mostly blame it on
The underlying problem is that old stream references repeat their monadic action when called, meaning that any action can be repeated again, leading to almost arbitrary results if one is not careful. This is not limited to IO, but applies to any monadic action! This means that whatever you can do with a monad,
streaming could repeat where you least expect it. How could we eliminate this problem?
With linear types of course! This is a perfect example of where non-linearity can lead to errors, even in a setting as strict as Haskell, if one is not careful. If the
streaming combinators would return linear stream references, errors like this would be caught at compile time; coincidentally this is exactly what I will be doing for the rest of the summer!
Further example of vulnerability
The example from above can be modified to read the whole file, from a stream only containing two lines. This is because the monadic action at the head of
s reads a line from that file, and since we didn’t close the file handle (by calling
next again on
s') we can keep grabbing lines by repeating that action.