"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.
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 (
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
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+ >>> 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.