LINEAR USAGE OF STATE
LINEAR USAGE OF STATE
复制标题
DOI：
10.2168/lmcs-10(1:17)2014
复制
发表时间：
2014-01-01
影响因子：
0.6
通讯作者：
Staton, Sam
中科院分区：
文献类型：
--
作者：
Mogelberg, Rasmus Ejlers;Staton, Sam
我们研究每个单子都是线性状态单子的现象。我们通过研究从不纯的按值调用语言到新的线性类型理论的完全完整的状态传递翻译来做到这一点：丰富的按值调用演算。结果并不特定于存储，但可以应用于使用代数运算可表达的任何计算效果，甚至应用于通常不被认为是有状态的效果。源语言中的通用效果与丰富的按值调用演算中的状态访问操作之间存在双射对应关系。从分类模型的角度来看，丰富的按值调用演算建议对有效按值调用语言的传统 Kleisli 模型进行改进。新模型可以理解为丰富的附加物。
We investigate the phenomenon that every monad is a linear state monad. We do this by studying a fully-complete state-passing translation from an impure call-by-value language to a new linear type theory: the enriched call-by-value calculus. The results are not specific to store, but can be applied to any computational effect expressible using algebraic operations, even to effects that are not usually thought of as stateful. There is a bijective correspondence between generic effects in the source language and state access operations in the enriched call-by-value calculus. From the perspective of categorical models, the enriched call-by-value calculus suggests a refinement of the traditional Kleisli models of effectful call-by-value languages. The new models can be understood as enriched adjunctions.