I will show how the problem of finding an optimal translation from the
(typed) lambda calculus into the linear lambda calculus can be reduced to
finding a "minimal" solution of a system of inequations over a 2-point
poset. To do this in a simple way I will introduce an alternative syntax of
a (suitable) fragment of Plotkin's DILL (dual intuitionistic linear logic)
that decorates types with annotations instead of relying on an separate
modality. I shall then describe how this simple idea finds its way into an
optimising compiler as an inference-based (static) analysis technique.
Unfortunately, linearity is not as useful as it might first seem, so I will
show how to relax the system in at least two different ways as well as hint
at the problems of taking linearity seriously to inform optimisations like
destructive updating, sharing and inlining. I will provide some (I hope
illuminating) working examples.