一句话:用函子范畴上的 monad 给出可含环引用单元的指称语义,并支持效应屏蔽与代码变换验证。
本文研究动态分配、且可能形成环形结构的引用单元的指称语义问题,特别关注局部状态封装(效应屏蔽)的语义刻画。作者将堆(heaps)视为某个函子范畴中的对象,并在其上构造一个用于为堆添加隐藏/封装能力的 monad;随后通过将状态 monad 变换器作用于该封装 monad,得到支持效应屏蔽的完全基类型引用(full ground references)的 monad。为评估该 monad,作者为一个带完全基类型引用的 call-by-value 演算给出了指称语义,并据此验证了相关的代码变换(等式推理)。该工作为含共享与环的内存单元提供了一种范畴论式的统一语义框架。
We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.