Effect Systems Revisited - Control-Flow Algebra and Semantics
Effect Systems Revisited - Control-Flow Algebra and Semantics
复制标题
重温效应系统 - 控制流代数和语义
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
T. Petříček
中科院分区：
文献类型：
--
作者：
A. Mycroft;Dominic A. Orchard;T. Petříček
效果系统最初被设想为基于推理的程序分析，以捕获程序行为-作为一组效果表示。此后发生了两个正交的发展。首先，出于静态分析的动机，效果被推广到代数中的值，以更好地建模控制流，例如可能/必须分析和并发性。第二，受语义问题的启发，基于集合或半格的效果系统的句法概念与单子的语义概念联系在一起，最近又与分级单子联系在一起，分级单子给出了效果的更精确的语义描述。
我们给出了一个轻量级的教程解释这两个线程中所涉及的概念，然后通过一个控制流代数的效果导向语义的概念将它们统一起来。对于有效的编程与排序，交替和并行的情况下-说明与音乐-我们确定了一种形式的分级joinads作为统一的效果分析和语义的适当结构。
Effect systems were originally conceived as an inference-based program analysis to capture program behaviour--as a set of representations of effects. Two orthogonal developments have since happened. First, motivated by static analysis, effects were generalised to values in an algebra, to better model control flow e.g. for may/must analyses and concurrency. Second, motivated by semantic questions, the syntactic notion of set- or semilattice- based effect system was linked to the semantic notion of monads and more recently to graded monads which give a more precise semantic account of effects.
We give a lightweight tutorial explanation of the concepts involved in these two threads and then unify them via the notion of an effect-directed semantics for a control-flow algebra of effects. For the case of effectful programming with sequencing, alternation and parallelism--illustrated with music--we identify a form of graded joinads as the appropriate structure for unifying effect analysis and semantics.