Clojure中codata示例的术语

Question

Clojure中codata示例的术语

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)

假设：

我们将pithy definition of codata视为“Codata是由可能是无限的值所居住的类型”。
这个Clojure例子没有使用静态类型系统（来自core.typed），因此对于codata的任何描述都是“工作定义”

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

- hawkeye

这是一个懒（无限）序列，它是codata。 - dorchard

1

这个问题可能更适合于http://programmers.stackexchange.com/。 - A. Webb

2个回答

0

我个人认为，对lazy-cons的调用返回值是所讨论的事物类型首次被认为是无限的点，因此这是我看到codata开始的地方。

- Arthur Ulfeldt

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Brian McKenna · Accepted Answer

Codata 是 Data 的对偶概念。通过结构归纳你处理有限的 data。通过余归纳你处理可能是无限的Codata（但不总是）。

无论如何，如果你不能适当地定义一个有限的 toString 或相等性，那么它就是 Codata：

我们能定义无限流的 toString 吗？不能，我们需要一个无限的字符串。
我们总能为两个无限流定义外延相等性吗？不能，那将永远需要时间。

我们无法为流执行上述操作，因为它们是无限的。但即使是潜在的无限也会导致不可判定性（即我们无法明确地给出相等性的答案或者无法明确地给出一个字符串）。所以无限的流是 Codata。我认为您的第二个问题更有趣，函数是 codata 吗？

Lisper 说“代码即数据”，因为 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的一些资源：