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!

• extract : w a -> a
$$!A \vdash A$$
This is the $$(read)$$ rule from linear logic.
• extend : (w a -> b) -> w a -> w b:
$$!A \multimap B \vdash !A \multimap !B$$