clojure - Clojure 中 codata 示例的术语

Question

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

(def fib-seq
  (concat
   [0 1]
   ((fn rfib [a b]
        (lazy-cons (+ a b) (rfib b (+ a b)))) 0 1)))

user> (take 20 fib-seq)
(0 1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 4181)

假设

我们取pithy definition of codata因为“Codata 是由可能是无限的值所占据的类型”。

这个 Clojure 示例不使用静态类型系统(来自 core.typed)，因此对 codata 的任何描述都是“工作定义”

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

Answer 1

Codata 是数据的对偶。您通过结构归纳处理数据，这意味着数据始终是有限的。您通过联合归纳处理 codata，这意味着 codata 可能是无限的(但并非总是如此)。

在任何情况下，如果您不能正确定义有限的 toString 或相等，那么它将是 codata:

我们可以为无限流定义一个 toString 吗？不，我们需要一个无限的字符串。

我们可以总是定义两个无限流的外延相等吗？不，那会花很长时间。

我们不能对流执行上述操作，因为它们是无限的。但即使是潜在的无限也会导致不可判定性(即我们不能给出明确的是或否的相等性，或者肯定地给出一个字符串)。

所以无限流是codata。我觉得你的第二个问题更有趣，是函数codata吗？

Lispers 说代码就是数据，因为像 S 表达式这样的特性允许像数据一样操作程序。很明显，我们已经有了 Lisp 的字符串表示(即源代码)。我们还可以使用一个程序并检查它是否由相等的 S 表达式组成(即比较 AST)。数据!

但是让我们停止考虑代表我们代码的符号，而是开始考虑我们程序的含义。取以下两个函数:

(fn [a] (+ a a))
(fn [a] (* a 2))

它们对所有输入给出相同的结果。我们不应该关心一个人使用 *其他用途 + .不可能计算任何两个任意函数是否在外延上相等，除非它们只适用于有限数据(相等只是比较输入-输出表)。数字是无限的，所以仍然不能解决我们上面的例子。

现在让我们考虑将函数转换为字符串。假设我们可以在运行时访问函数的源代码表示。

(defn plus-two [a] (+ a 2))
(defn plus-four [a] (plus-two (plus-two a)))
(show-fn plus-four)
; "(plus-two (plus-two a))"

现在，引用透明说我们可以将函数调用替换为函数体，替换变量并且程序总是给出相同的结果。让我们为 plus-two 这样做:

(defn plus-four [a] (+ (+ a 2) 2))
(show-fn plus-four)
; "(+ (+ a 2) 2)"

哦……结果不一样。我们打破了引用透明度。

所以我们也不能为函数定义 toString 或等式。那是因为它们是codata!

以下是我发现有助于更好地理解 codata 的一些资源:

Data, Codata, and Their Implications for Equality, and Serialization

Codata and Comonads in Haskell

Data and Codata on A Neighborhood of Infinity

Some slides from University of Nottingham