论文标题
一个完全可预测的结果：研究无限结构的遍历
A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures
论文作者
论文摘要
可以将具有可穿越类型类实例的函子视为允许元素遍历的数据结构。这是通过可遍布的函子和限制容器（也称为多项式函数）之间的对应关系来确切的，这是在总计（必然终止）函数的背景下建立的。但是，Haskell语言是非局部性的，并且允许不终止的功能。长期以来，人们一直观察到，遍历有时可以实际上在无限列表上运行，例如在分发读取器应用程序中。这种遍历的结果仍然是无限的结构，但是它仍然是有效的 - 即连续数量的有限计算产量终止或连续的结果。为了调查这一现象，我们利用了直接在Haskell中使用方程推理来利用来自保护的递归中的工具。
Functors with an instance of the Traversable type class can be thought of as data structures which permit a traversal of their elements. This has been made precise by the correspondence between traversable functors and finitary containers (also known as polynomial functors) -- established in the context of total, necessarily terminating, functions. However, the Haskell language is non-strict and permits functions that do not terminate. It has long been observed that traversals can at times in fact operate over infinite lists, for example in distributing the Reader applicative. The result of such a traversal remains an infinite structure, however it nonetheless is productive -- i.e. successive amounts of finite computation yield either termination or successive results. To investigate this phenomenon, we draw on tools from guarded recursion, making use of equational reasoning directly in Haskell.
