完全可预测的结果：无限结构遍历的调查
计算机科学中的逻辑
2022-07-21 v1 编程语言
摘要
具有 Traversable 类型类实例的函子可被视为允许遍历其元素的数据结构。这已由可遍历函子与有限容器（亦称多项式函子）之间的对应所精确化——该对应在总体、必然终止的函数背景下建立。然而，Haskell 语言是非严格的且允许不终止的函数。长期以来人们观察到遍历事实上有时可对无限列表操作，例如在分发 Reader 应用函子时。此类遍历的结果仍是无限结构，但其仍是生产性的——即有限的连续计算产生终止或连续结果。为研究此现象，我们借助守卫递归的工具，直接在 Haskell 中使用等式推理。
引用
@article{arxiv.2207.10010,
title = {A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures},
author = {Gershom Bazerman},
journal= {arXiv preprint arXiv:2207.10010},
year = {2022}
}