Understanding idiomatic traversals backwards and forwards
Understanding idiomatic traversals backwards and forwards
复制标题
理解惯用的前后遍历
DOI：
10.1145/2503778.2503781
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Bird R
中科院分区：
文献类型：
--
作者：
Bird R
我们提出了对特定类别的有效 Haskell 程序进行推理的新方法，即那些表示为惯用遍历的程序。从有关标记和取消标记二叉树的特定问题开始，我们提取适用于任何单子的通用反转定律，将对任意可遍历类型的元素的遍历与相反方向的遍历相关联。可以援引该定律来表明，在适当的意义上，取消标签是标签的逆过程。反转律以及惯用遍历的许多其他属性是一个更一般定理的推论，该定理将可遍历函子描述为有限容器：任意可遍历对象可以唯一地分解为形状和内容，并且可以根据这些来理解遍历。该定理的证明涉及与自由应用函子相关的特殊习语中的遍历属性。
We present new ways of reasoning about a particular class of effectful Haskell programs, namely those expressed as idiomatic traversals. Starting out with a specific problem about labelling and unlabelling binary trees, we extract a general inversion law, applicable to any monad, relating a traversal over the elements of an arbitrary traversable type to a traversal that goes in the opposite direction. This law can be invoked to show that, in a suitable sense, unlabelling is the inverse of labelling. The inversion law, as well as a number of other properties of idiomatic traversals, is a corollary of a more general theorem characterising traversable functors as finitary containers: an arbitrary traversable object can be decomposed uniquely into shape and contents, and traversal be understood in terms of those. Proof of the theorem involves the properties of traversal in a special idiom related to the free applicative functor.
登录
查看更多内容
影响因子：
0.8
作者：
GIRARD, JY
通讯作者：
GIRARD, JY
Monad、形状函子和遍历
影响因子：
4.6
作者：
E. Moggi;Gianna Bellè;C. Jay
通讯作者：
C. Jay
影响因子：
4.6
作者：
Mauro Jaskelioff;Ondrej Rypacek
通讯作者：
Ondrej Rypacek
涉及类型构造函数类的自由定理
影响因子：
4.6
作者：
F. Pearl;Janis Voigtl
通讯作者：
Janis Voigtl
涉及类型构造函数类的自由定理：函数珍珠
影响因子：
4.6
作者：
J. Voigtländer
通讯作者：
J. Voigtländer