"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

LZ4_LIB_API size_t LZ4F_decompress(LZ4F_dctx* dctx,
                                   void* dstBuffer, sizet* dstSizePtr,
                                   const void* srcBuffer, sizet* srcSizePtr,
                                   const LZ4F_decompressOptions_t* 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.