问题标签 [codata]

就简洁的摘要而言——对 Comonads 的这种描述似乎更胜一筹——将它们描述为“输入杂质的类型”。

什么是 codata 的等效简洁（单句）描述？

想象一下在 Clojure 中给出一个无限惰性斐波那契序列的函数：

假设

1. 我们将 codata 的简洁定义视为“Codata 是由可能是无限的值所占据的类型”。
2. 这个 Clojure 示例不使用静态类型系统（来自 core.typed），因此任何对 codata 的描述都是“工作定义”

我的问题是 - 上面函数的哪一部分是“codata”。是匿名函数吗？是惰性序列吗？

这里有一些解释。直觉上，我理解有限数据结构与流等无限数据结构有何不同。然而，有趣的是看到其他对差异、特征和余数据类型的解释。

在阅读有关流时，我偶然发现了 codata 术语。

我们不能以无限精度存储小数，但可能有某种方式来表示它们，就像我们在 haskell 中表示无限列表一样。

我想到的第一个想法是通过类似于Codata的东西来表示一个十进制数，这样对于任何给定的自然数 k，我们都可以计算出精确到 k 位的十进制数。

但是有一个明显的问题，想想数字a = 0.333...和b = 0.666...，如果我们把它们加在一起，我们得到ans = 0.999...(a sequence of numbers) ，但我们永远无法判断是否a + b == 1在这种情况下。

我想要的是，以某种方式定义十进制数，使其支持+, -, *, /, >,==操作，无论我们对这些十进制数应用什么+, -, *,/操作，我们都会得到新的十进制数，我们可以计算它们给定任何自然数 k，精确到 k 位。

我想知道：有什么想法可以解决这个问题吗？

filter : (a -> Bool) -> List a -> List aList 有，Stream 没有，filter : (a -> Bool) -> Stream a -> Stream a为什么？

有没有其他方法可以做类似的工作？

我发现Lazy并且Inf非常接近：

Lazy 和 Inf 密切相关（实际上底层实现使用相同的类型）。实践中的唯一区别是整体检查，其中 Lazy 被擦除（即，正常检查术语是否终止，忽略惰性注释），而 Inf 使用生产力检查器，其中任何使用 Delay 都必须受到构造函数的保护。

如上所述，Lazy和的底层实现Inf是相同的，唯一的区别是关于整体检查。

我认为 always useInf看起来更自然，这更接近我们在 Haskell 中使用的 lazy，并且想知道我们必须使用的生产场景是什么Lazy——它总是做深度的整体检查？

我正在尝试实现一种表示无限二叉树上（可能）无限路径的类型。当前的定义类似于标准库中的Conat。

现在我想定义一个重复部分更长的值，例如 LRRL。我现在能写的最好的是以下（很快就会变得乏味）。

目标

定义branchL'和branchR'使以下通过类型检查和终止检查。

到目前为止我尝试过的事情

将部件包装在常规函数中不起作用：

所以我尝试包装成一个宏，但我找不到如何构造这个术语branchL λ where .force → pathwhen pathis given as a Term。以下也不起作用：

我正在试验Jesper Cockx 和 Andreas AbelCoNat的这篇论文中的定义：

我定义zero和plus：

我定义了双相似性：

但我坚持plus zero n与n. 我的猜测是，在证明中我应该（至少）有一个 with 子句iszero n：

但是 Agda 抱怨以下错误消息：

我怎样才能做出这个证明？

Corecursion 意味着在每次迭代中调用自己的数据大于或等于以前的数据。Corecursion 适用于 codata，它们是递归定义的值。不幸的是，值递归在严格评估的语言中是不可能的。不过，我们可以使用显式的 thunk：

虽然这按预期工作，但方法似乎很尴尬。尤其是可怕的对元组让我很恼火。有没有更自然的方法来处理 JS 中的 corecursion/codata？

这是一个核心递归算法，因为每次迭代它都会调用比之前更大的数据：

它类似于尾递归累加器样式，但它的累加器是隐式的，而不是作为参数传递。如果不是因为懒惰，它将是无限的。那么 codata 是否只是 WHNF 中的值构造函数的结果，有点像(a, thunk)？或者 codata 是范畴论中的一个数学术语，在编程领域没有有用的表示？

后续问题：值递归只是核心递归的同义词吗？