Functional models of full ground, and general, reference cells
We present ongoing work developing a straightforward denotational semantics for reference cells of arbitrary types based on sets- with-structure and structure-preserving functions. We start with full ground references — which can refer to ground values and (recursively) ground references — where types denotes set-valued presheaves. By considering stores as mixed-variance set-valued functors (i.e., profunctors), we obtain two monads for full ground state which can interpret alloction, dereference, and mutation of full ground references, while validating the usual equations. We use this structure to give a denotational semantics to a monadic metalanguage with a special construct for effect masking similar to Haskell’s runST. Time permitting, we speculate how to extend this approach, using an appropriate recursive domain equation, to account for ML-like general reference cells.