Терминология на примере кодаты в Clojure
Вообразите следующую функцию, чтобы дать бесконечную ленивую последовательность Фибоначчи в 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)
Если предположить,
- Мы принимаем содержательное определение кодаты как "Кодаты - это типы, населенные значениями, которые могут быть бесконечными".
- То, что этот пример Clojure не использует статическую систему типов (из core.typed), и поэтому любое описание codata является "рабочим определением"
У меня вопрос - Какая часть функции выше - это "кодата". Это анонимная функция? Это ленивая последовательность?
2 ответа
Кодата - это двойник данных. Вы работаете с данными через структурную индукцию, что означает, что данные всегда конечны. Вы работаете с кодатами через коиндукцию, что означает, что кодаты потенциально бесконечны (но не всегда).
В любом случае, если вы не можете правильно определить конечное значение toString или равенство, тогда это будут кодаты:
- Можем ли мы определить toString для бесконечных потоков? Нет, нам нужна бесконечная строка.
- Можем ли мы всегда определять экстенсиональное равенство для двух бесконечных потоков? Нет, это займет вечность.
Мы не можем сделать выше для потоков, потому что они бесконечны. Но даже потенциально бесконечные причины неразрешимости (то есть мы не можем дать однозначное да или нет за равенство или определенно дать строку).
Итак, бесконечный поток - это кодата. Я думаю, что ваш второй вопрос более интересен, функция codata?
Лисперс говорит, что код - это данные, потому что такие функции, как 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'nes.