13 March 2017|
We're extending GHC with linear types.
Ever since Jean-Yves Girard discovered linear logic in 1986, researchers around the world have been going "wow! resource tracking, this must be useful for programming languages". After all, any real computation on a real machine takes resources (memory pages, disk blocks, interrupts, buffers etc) that then aren't available anymore unless restored somehow. But despite this match apparently made in heaven, research on this subject has remained largely theoretical. It was becoming easy to just give up and assume this nut was simply too tough to crack. We ourselves have been there, but we recovered: we're having a go at extending GHC with linear types.
Great! But why is this useful in a high-level programming language like Haskell? You'll find the long of it in the paper we just submitted to ICFP'17 with Mathieu Boespflug, Ryan Newton and Simon Peyton Jones. In this blog post, we'll briefly discuss (more in the paper) how we're trying to achieve more predictable performance at a smaller memory footprint in Haskell, and give you a preview of what you might expect in your favourite compiler in the not-so-distant future.
Once upon a time, Jean-Yves Girard was playing with ways to describe the semantics of a λ-calculus with types, when he realised that from a semantic perspective there was nothing essential about the arrow type (the type for functions): it could be described in terms of two simpler constructions. He followed this thread through and came up with a strange beast he called linear logic.
Linear logic had two of everything: two ways of building conjunctions and disjunctions, two notions of truth, falsehood and two ways to negate. It's a strange system, but perhaps not moreso than the zoo of cute names and symbols Girard conferred to every construct. For the purposes of this post, we'll only need one new symbol from this zoo: $⊸$, which reads lollipop (also called linear arrow, or lolly for close friends).
If we transpose linear logic to describing the behaviour of programs (by which point we talk about linear types), the linear arrow says this: a function that has type $A⊸B$ is a function that has an $A$ available to compute with, but it can only use it once. Not twice, not zero times: just once. It turns out that this property, which has come to be known as linearity, is very useful for compilers of functional programs.
Programming language researchers quickly took notice. It was not long before Yves Lafont proposed a language with safe memory management yet without needing a garbage collector, thanks to linear types. Philip Wadler piled on a few years later with a system also supporting state update while retaining the properties of a pure language. Recently, researchers have even pushed linear logic towards making it possible to reason about pointer aliasing (the absence or presence of aliasing matters a lot in the optimization and the correctness of C programs).
But despite all these early promises (and many more since then), linear types didn't catch on in the mainstream. Mind you, there have been workarounds. It turns out linear types are also useful to model effects, but Haskell preferred monads for that purpose instead. Clean wanted safe mutable state, but eschewed monads, using uniqueness types instead. More recently, Rust rose to popularity with a system of ownership which is not unlike Clean's uniqueness types. Both are complex systems that permeate the entire language and ecosystem in ways that make the learning curve pretty steep.
What if you could enjoy all your favourite goodies from your favourite programming language, and yet be able to leverage linear types for precise resource management exactly where it matters (as Lafont did by avoiding garbage collection)? The result won't be as good as Rust for what Rust does: it's a different trade-off where we assume that such precision is only needed in small key areas of a program that otherwise freely uses functional programming abstractions as we know them today.
This is what we are proposing: a simple, unintrusive design that can be grafted to your favourite functional language at no cost for the programmer. We're working on GHC, but this would work just as well in your favourite ML flavour.
Among our many projects, we are working together with Seagate and a number of consortium partners on the SAGE platform, an EU funded R&D project exploring how to store massive amounts of data (in excess of one exabyte) and query this data efficiently. We use Haskell as a prototyping language to fail fast when we're heading towards a dead end, backtrack and explore a different direction at low cost, and refactor our existing code easily when we commit to a different direction.
On this and other systems level projects, maintaining predictable latencies is key. Pusher recently documented how this matters to them too, to the point where they've been looking elsewhere for good latencies. Our use cases share the same characteristics. We decided to solve the problem by asking less of the GC, while extending Haskell to make working outside of the GC just as memory safe. You will find much more details in the paper, but in summary linear types help in two ways:
malloc: because linearity forces the programmer using a value at least once, we can ensure that the programmer eventually calls
free. And because it forces to use a value at most once, we can make sure that
free-d data is never used (no use-after-free or double-free bugs). Anything that we
mallocexplicitly doesn't end up on the GC heap, so doesn't participate in increasing GC pause times.
But the story gets better still. Linear types aren't only useful for performance, they can also be key to correctness. SAGE is a complex project with many communicating components. Linear types allow us to model these interactions at the type level, to statically rule out bugs where some component doesn't respect the protocol that was agreed upon with others. We don't talk about that much in the paper, but we'll touch on that here.
Let's start slow, with the
fst function projecting the first
component from a pair:
fst :: (a,b) -> a fst (x,_) = x
So far, so standard. Now here is a new thing you cannot do:
fst :: (a,b) ⊸ a fst (x,_) = x
This $⊸$ is the linear arrow: the type of functions which must use their arguments exactly once. The first projection is not linear, since a part of the pair is silently dropped. So the type checker will reject this program. It will also reject the diagonal, which uses its argument twice:
dup :: a ⊸ (a,a) dup x = (x,x)
On the surface, this is almost the entire story: the linear arrow
allows you to reject more programs, of which
With that in mind, there's a lot that linear types can be used for. One example is strongly typed protocols that check applications in a distributed system interact as expected. We'll need a little bit of kit first:
data S a data R a newCaps :: (R a ⊸ S a ⊸ IO ()) ⊸ IO () send :: S a ⊸ a ⊸ IO () receive :: R a ⊸ (a ⊸ IO ()) ⊸ IO ()
In this API,
S is a send capability: it gives the ability to send
R is a receive capability. A pair of corresponding
capabilities is allocated by
newCaps. The important thing to notice
is that since both capabilities are linear, both must be consumed
exactly once by a
send and a
receive respectively. Conversely, you
can't send/receive without having a corresponding send/receive
capability on hand.
As a first example, let's consider a protocol where a server expects
two integers and returns the sum to the client. A simple function,
except happening across a wire. This protocol is fully captured by the
(Int, Int, Int ⊸ IO ()), which reads: receive two
⊸ IO () switches between "send" and "receive".
To implement a protocol
P, one has to write an implementation (a
function) of type
P ⊸ IO (). The other side of the wire (the client)
must implement the dual protocol
P ⊸ IO (), with a function of type
(P ⊸ IO ()) ⊸ IO ():
type P = (Int, Int, Int ⊸ IO ()) server :: P ⊸ IO () server (n, p, k) = k (n + p) client :: (P ⊸ IO ()) ⊸ IO () client sendToSrvr = newCaps $ \r s -> do sendToSrvr (42, 57, send s) receive r (\n -> print n)
We can see how typing works:
client must create a function
Int ⊸ IO () for the server to send its result to. So it creates an
pair, into which the server will be able to send exactly one result.
r capability must also be consumed exactly once. Therefore, the
client must call
receive and do something with the result (in this
case, it boringly prints it on a console).
Of course, one can replace all the linear arrows with regular arrows
-> and the program stays well-typed. But the value of linear types
lies in what they do not allow:
client cannot forget to call
receive, resulting in the server blocking on
send; similarly, the
server is not allowed to return twice to
k (n+p) >> k (n*p) is not well-typed). This prevents all sort of bad
behaviours. It is not a novel idea; see the paper's "related work"
section if you're interested in the references.
To run the server and the client, we must assume an initial
r0 (known only to the runner, for safety):
runServer :: IO () runServer = receive r0 server runClient :: IO () runClient = client (send s0)
We can make more complex examples by alternating the
⊸ IO ()
construction to sequence the steps of the protocol. For instance, the
following asks first for a number, then the word "apple" singular or
pluralized, depending on the number, and returns a sentence:
data Number = Singular | Plural type P = (Int, (Number, (String, String ⊸ IO ()) ⊸ IO ()) ⊸ IO ()) server :: P ⊸ IO () server (n, k) = newCaps $ \r s -> do k (num, send s) receive r $ \(apples, k') -> do k' ("I have " ++ show n ++ apples) where num = if n == 1 then Singular else Plural client :: (P ⊸ IO ()) ⊸ IO () client k = newCaps $ \r s -> do k (42,send s) receive r $ \(num,k') -> newCaps $ \r' s' -> do let apples | Singular <- num = "apple" | Plural <- num = "apples" k' (apples, send s') receive r' $ \sentence -> print sentence
Running the server and client will result in the client printing the
deliciously healthy sentence "I have 42 apples". Again, the value is
in what is rejected by the compiler, such as listening to
r a second
time in the client rather than to
An important takeaway is how haskelly this all looks: just replace
⊸ and linearity kicks in. Usual datatypes, including tuples,
take a linear meaning in a linear context. The technical details of
how this is achieved are exposed in the article. Edsko de
Vries wrote a blog post where he compares the trade-offs
of related type systems; he comes in favour of a system where types
are segregated into linear types and unrestricted types, but our
position is that such a system, perhaps more flexible, would be more
complex to implement, especially if we want good sharing of code
between linear and non-linear contexts.
One thing that the article does not have, however, is a good description of how our prototype implementation (and type inference) works.
Yes! There is a branch of GHC where we are implementing
the above proposal. At the time of writing the prototype is still
a bit crude: it handles the λ-calculus fragment properly, but
data do not have full support yet. We believe we have the hard
part behind us though: modifying the arrow type so that arrows carry
an annotation discriminating whether they are regular arrows (
linear arrows (
Indeed, GHC uses and abuses the arrow type all over the type inference mechanism. So making a change there required changes across many files. As it turns out, however, the changes are rather systematic and innocuous. The patch is currently under 1000 lines long. We are targeting a merge by the time of the 8.4 release of GHC.
In a future post, we'll delve into what the paper doesn't cover, to show how inferring linear types works.