"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, size*t* dstSizePtr,
const void* srcBuffer, size*t* 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.