"Linear Types can change the world." Lafont has shown us how to create a linear abstract machine. Yet the moral imperative to use linear types in computer science is not widely appreciated.

Logic & Computation

The Curry-Howard correspondence tells us that evaluation of functional programs corresponds to proofs of propositions.

But the thing in question (algorithms, procedures) is morally different from propositions in logic. Procedures relate a class of inputs to outputs, while theorems often stand as values themselves. The complexity of such procedures enforces a qualitative difference, which we do not distinguish in the world of theorems.

So, what is the type of a computation? Girard's linear logic distinguishes between an object factory and an object.

The C procedure

LZ4FLIBAPI sizet LZ4Fdecompress(LZ4Fdctx dctx, void dstBuffer, sizet dstSizePtr, const void srcBuffer, sizet srcSizePtr, const LZ4FdecompressOptionst dOptPtr);

for instance, takes an object (dctx), while the Haskell function

cycle :: [a] -> [a] cycle [] = undefined cycle xs = xs' where xs' = xs ++ xs'

takes an object factory (xs).

Mutability & Object Factories

Imperative languages (with mutation) fall over when they try to ape the intuitionist typing of (immutable) functional languages. Intuitionist typing remains in linear logic; we translate the type A to type !A (i.e. an object factory).

In Haskell one can write

cycle :: [a] -> [a]

without any problem (in linear logic, we would consider Haskell values, managed by the garbage collector, to be factories).

>>> a=[1,2,3] >>> b=a >>> a=a+[1] >>> a [1, 2, 3, 1] >>> b [1, 2, 3]

Mutation demands an object (i.e. the full linear logic). If we pretend to type like the functional languages (as Python does), what we are doing is appending a mutation onto an object factory - a mess.