首页    期刊浏览 2024年11月14日 星期四
登录注册

文章基本信息

  • 标题:Linear usage of state
  • 本地全文:下载
  • 作者:Rasmus Møgelberg ; Sam Staton
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2014
  • 卷号:10
  • 期号:1
  • 页码:1
  • DOI:10.2168/LMCS-10(1:17)2014
  • 出版社:Technical University of Braunschweig
  • 摘要: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.
  • 其他关键词:Linear type theory, monads, computational effects, categorical semantics, enriched category theory, state passing translation.
国家哲学社会科学文献中心版权所有