Терминология для примера КОДАТА в Clojure

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) 

Предполагая

1. Мы принимаем pithy definition of codata как «КОДАТА типы обитаемые по значениям, которые могут быть бесконечными ».
2. Вот этот пример Clojure не использует статическую систему типов (от core.typed), и поэтому любое описание КОДАТА является «рабочее определение»

Мой вопрос - Какая часть функции выше «codata». Это анонимная функция? Это ленивая последовательность?

Answer 1

Codata - это двойник данных. Вы работаете с данными через структурную индукцию, что означает, что данные всегда конечны. Вы работаете с codata через coinduction, что означает, что codata потенциально бесконечна (но не всегда).

В любом случае, если вы не можете правильно определить конечную ToString или равенство, то это будет КОДАТА:

• Можем ли мы определить ToString для бесконечного потока? Нет, нам нужна бесконечная строка.
• Можем ли мы всегда определять экстенсиональное равенство для двух бесконечных потоков? Нет, это навсегда.

Мы не можем сделать выше для потоков, потому что они бесконечны. Но даже потенциально бесконечные причины неразрешимости (то есть мы не можем дать определенное да или нет для равенства или определенно дать строку).

Таким образом, бесконечный поток - это codata. Я думаю, что ваш второй вопрос более интересен, есть функция codata?

Лисперс говорит, что код - это данные, поскольку такие функции, как S-выражения, позволяют манипулировать программой точно так же, как данные. Очевидно, что у нас уже есть строковое представление Lisp (то есть исходный код). Мы также можем взять программу и проверить, состоит ли она из равных S-выражений (т. Е. Сравнить AST). Данные!

Но давайте перестанем думать о символах, представляющих наш код, и вместо этого начнем думать о , что означает наших программ. Возьмите следующие две функции:

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

Они дают одинаковые результаты для всех входов. Нам все равно, что один использует *, а другой использует +. Невозможно вычислить, являются ли какие-либо две произвольные функции extally равными, если только они не работают только с конечными данными (равенство тогда просто сравнивает таблицы ввода-вывода). Числа бесконечны, так что все еще не решает наш вышеприведенный пример.

Теперь давайте подумаем о преобразовании функции в строку. Допустим, у нас был доступ к исходному представлению функций во время выполнения.

(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 или равенство для функций. Это потому, что они кодаты!

Вот некоторые ресурсы, которые я нашел полезный для понимания КОДАТА лучше:

• 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

Answer 2

Мое личное мнение Возвращаемое значение звонка на ленивые-минусы - это точка, в которой тип вещи, о которой идет речь, можно было бы назвать инфинитной, и, таким образом, это то, что я вижу, начинаются.