5

想象一下在 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)

假设

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

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

4

2 回答 2

10

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

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

  • 我们可以为无限流定义一个 toString 吗？不，我们需要一个无限的字符串。
  • 我们总是可以为两个无限流定义外延相等吗？不，那需要永远。

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

所以无限流是余数据。我觉得你的第二个问题更有趣，是函数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 的一些资源：

于 2013-07-13T03:21:57.443 回答
0

我个人的想法是调用lazy-cons 的返回值是所讨论事物的类型首先可以说是无限的点，因此这就是我看到codata'nes 开始的点。

于 2013-07-12T17:27:31.183 回答