Pull to refresh

Comments 11

БрррРр. Мега, конечно. Особенно рассуждение о производных. Но чтобы народ въехал, imho, следует сначала привести пример использования zipperа. Это 1.\

2. Фраза 'то есть ровно то, что у нас и было'. Внимательно перечитал два раза — не было. Точнее, было, но не в формальной записи. Опять же запутывает процесс чтения.

3. Неплохо бы было перед началом манипулирования производной, хотя бы примерно указать на то, что множества значений типов относительно операций + и * составляют кольцо. Следовательно, можно рассматривать многочлены с производными. А то какой-то слишком формальный переход получается.

Ну. А вообще, Haskell, как всегда, развивающе плющит мозг.
Жаль, уходить надо, исправлять придётся вечером.
1. Ну на практике я его и сам не использовал, разве что Вы просто о примере в виде кода, как пройтись туда-обратно и поменять пару значений. Следует добавить, согласен.
2. Спасибо, не обратил внимания даже при нескольких перечитываниях, исправлю.
3. Даже дифференциальное кольцо. Возможно, стоит упомянуть, но я не ставил целью математическую точность, так как сам не обладаю достаточными знаниями, а, упоминая о кольцах, рискую нарваться на сложные вопросы :)
> дифференциальное кольцо

Это колько с «дифференцированием» чтоли? Первый раз этот термин встречаю.
Не понятно, как понимать запись:
f(x) = 1 + x*f(x)

Как уравнение относительно x, где f известна, или как определение функции f. Если это определение, то еще нужно указать, где она определена, например, очевидно, что её значения в x=1 не существует. Так же если это определение, то непонятно, зачем вводить функцию h, которая задана так же.

Это именно уравнение, но это не уравнение для определения функции над полем действительных чисел. Это уравнение в алгебре типов с операциями + и *. Где, неточно говоря, тип A + B — это тип значениями которого могут быть значения типа A или значения типа B. А тип A * B, это тип со значениями (a, b), где a — значение типа A, а b — значение типа B. Эти операции позволяют записывать многочлены, вводить их производные и т.д. При этом, это уравнение не для поиска функции, а для поиска некоторого элемента в этой алгебре. f(x) — некоторое значение, а не отображение одних значений на другие (хотя, конечно, это значение можно интерпретировать, как программу для отображения).

Поэтому, для типа X, тождественно равного единице (в данном случае 1 — это такой тип, который содержит только одно значение и, следовательно, не содержит никакой информации), решением будет тип 'непустой список из одинаковых элементов': такой список — это или (1) просто одно значение, или (2) некоторое значение, за которым следует список из этих же самых значений, что можно записать в виде пары (v, 'непустой список из одинаковых элементов').

Вот такая занимательная арифметика.
f(x) — некоторое значение, а не отображение одних значений на другие

Если я все правильно понял, то как раз наоборот. f(x) — это отображение типа на тип, например, int в список int'ов.
Берем f(x)=1+x*f(x), это эквивалентно f(x)=1+x+x*x*f(x), и так далее получим:
f(x)=\sum_{n=1}^{\infty} x^n
И любой инстанс этого типа есть список объектов класса x. То тогда не понятно зачем вводить функцию h, такую же как и f.
1. Ну. Является ли многочлен отображением или конечной строчкой из коэффицентов? Зависит от того, как рассматривать. Тут же, скорее, синтаксические преобразования используются в решении уравнения, а не свойства отображения, как отображения. Я это имел в виду.

2. Там же задача не f(x) вычислить, а вычислить zipper от f(x). Можно доказать, что zipper для типа f(x) — это [x * f'(x)]. И теперь стоит задача выразить f'(x). Ради этого все преобразования и делаются.
Является ли многочлен отображением или конечной строчкой из коэффицентов?

Да, многочлен является отображением, да, многочлен представляется строчкой из коэффициентов=) Через синтаксические преобразования производная в кольце многочленов и вводиться в алгебре (никаких пределов!).

На самом деле статья путанная:
В начале говорим, что zipper для списков это A × (List A) × (List A), затем показываем, что (List A)'=(List A) × (List A) и, обобщая (без доказательства) говорим, что zipper для полиморфного типа F(X) есть X × F'(X). Даже само доказательство (List A)'=(List A) × (List A), imho, путаное, намного проще было бы так:

Определим список (эквивалентно f(x)=1+x*f(x)):
f(x)=\sum_{n=1}^{\infty} x^n

Посчитаем производную:
f'(x)=\sum_{n=1}^{\infty} n \cdot x^{n-1}

Далее очевидно (простые вычисления), что
\left(\sum_{n=1}^{\infty} x^n\right) \cdot \left(\sum_{n=1}^{\infty} x^n\right)=\sum_{n=1}^{\infty} n \cdot x^{n-1}

То, есть f'(x)=f(x)*f(x).
То, что zipper для F(X) есть X × F'(X) берётся без доказательства, т.е. это не вывод на основе списка, ибо производную я взял уже позже. Это просто бездоказательное утверждение в данном контексте.
h(x) я ввёл, чтобы вынести f(x) за пределы определения, а то, что h(x) оказалось списком — это счастливая случайность :)

Насчёт f(x) всё именно так
f(x) = 1 + x + x*x + x*x*x + x*x*x*x +…
Но ведь так и есть, список — это или пустой, или один элемент, или два, или… и так до бесконечности. f(1) не является конечным числом, но это и понятно, так как возможных списков явно не конечное число даже для типа с одним элементом. А вот f(0) = 1, т.е. для типа без элементов список может быть только пустым.
Only those users with full accounts are able to leave comments. Log in, please.