Linear logic is often introduced with unintuitive and contrived examples involving food. For computer scientists, linear logic is well motivated by memory management à la C.
In typical compiled languages, code is static and values are heap- or stack-allocated. Management of stack-allocated values is left to the compiler.
Heap-allocated values begin with malloc and end with free. Linear logic
requires that all values be consumed exactly once (motto: every question must
have an answer and every answer a question); one must free a value and
it can be freed only once. Thus, memory is not leaked and we do not have
double-free errors.
- \( A \) - the type of a heap-allocated value
- \( A \oplus B \) - a sum type
- \( A \otimes B \) - a strict pair, a product type. A tuple or a struct in C (for instance).
- \( !A \) - the type of a stack-allocated value (or the type of a static immutable value)
\( A \multimap B \) - \( A \multimap B \) comes up in currying and application. We can use the conventional arrow \(A \rightarrow B\) to denote "B is a consequent of A"; in this context it means we have a function to compute B from A.
If we have an uncurried function \(A \otimes B \rightarrow C \), we can curry to get \( A \rightarrow B \multimap C \). Curried functions can be applied, \( {\tt apply} : (A \multimap B) \otimes A \rightarrow B \).
This makes sense: a partially applied function might be returned as a closure. This closure would reference \(A\) but \(A\) would not be consumed until the function was called. One might leak space if such functions were taken to be like the static procedures that are compiled.
For a standard C program:
int main(void);
In linear logic, the type of main would be 𝟙 → !Int. Some more examples:
void free(void *ptr);
VoidPtr → 𝟙
void *malloc(size_t size);
!Size → VoidPtr
void *realloc(void *ptr, size_t size);
(VoidPtr ⊗ !Size) → VoidPtr
