Skip to main content

A monad for full ground reference cells

Ohad Kammar ( Department of Computer Science, University of Oxford )

I will describe how to build a monad on a functor category to model
dynamic allocation of potentially cyclic memory cells. In particular
I'll explain how to tackle the challenge of "effect masking" which
means roughly that "if you don't need to know about memory access then
you can't detect it.", and use this monad to give a denotational
account of an ML-like language with reference cells, and validate
associated program transformations.

I will explain the main insight behind our construction: identifying
the collection of stores as an object in a different functor category
equipped with a monad for adding hiding/encapsulation capabilities to
the stores. I will then obtain the full ground storage monad by
applying a state monad transformer to the encapsulation monad.

The talk is based on work with: Paul B. Levy, Sean K. Moss, and Sam
Staton (http://arxiv.org/abs/1702.04908).

Share this: