The !-modality is a comonad. In particular, it is a functor; we can lift any function/procedure to work on perennial types with map, \( A \multimap B \vdash !A \multimap !B \).
With our gloss, we can imagine that
map perennializes heap-allocated values: perhaps one has a function
manipulating heap-allocated records or sum types, and then map converts this
to a function operating on stack-allocated values whose lifetimes are managed by the compiler. I think this functorial approach would be very elegant in a compiler!
Look at the comonad interface as it is implemented in Haskell:
extract : w a -> a\( !A \vdash A \)
This is the \( (read) \) rule from linear logic.
It would correspond to converting a stack-allocated value (whose lifetime is managed by the compiler) to a heap-allocated value (say, by writing a value to a pointer).
extend : (w a -> b) -> w a -> w b:\( !A \multimap B \vdash !A \multimap !B \)
