术语,例如Clojure中的codata

Question

想象一下以下函数在Clojure中给出一个无限懒惰的fibonacci序列:

(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'.这是匿名函数吗？它是懒惰的序列吗？

Answer 1

Codata是数据的双重性.您通过结构归纳处理数据,这意味着数据始终是有限的.你通过coinduction使用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的资源:

• 数据,Codata及其对平等和序列化的影响
• Haskell中的Codata和Comonads
• 无限邻域的数据和Codata
• 一些幻灯片来自诺丁汉大学