VoidEx14 мая 2009 в 03:02

Zipper — производная от типа

5 мин

3.4K

Haskell *

+22

Комментарии 11

mikhanoid 14 мая 2009 в 03:54

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

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

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

Ну. А вообще, Haskell, как всегда, развивающе плющит мозг.

VoidEx 14 мая 2009 в 04:30

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

zw0rk 14 мая 2009 в 20:29

> дифференциальное кольцо

Это колько с «дифференцированием» чтоли? Первый раз этот термин встречаю.

VoidEx 14 мая 2009 в 20:32

Да, они

shai_xylyd 14 мая 2009 в 07:00

Не понятно, как понимать запись:

f(x) = 1 + x*f(x)

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

mikhanoid 14 мая 2009 в 07:45

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

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

Вот такая занимательная арифметика.

shai_xylyd 14 мая 2009 в 08:48

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.

mikhanoid 14 мая 2009 в 09:15

1. Ну. Является ли многочлен отображением или конечной строчкой из коэффицентов? Зависит от того, как рассматривать. Тут же, скорее, синтаксические преобразования используются в решении уравнения, а не свойства отображения, как отображения. Я это имел в виду.

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

shai_xylyd 14 мая 2009 в 09:53

Является ли многочлен отображением или конечной строчкой из коэффицентов?

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

На самом деле статья путанная:
В начале говорим, что 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).

VoidEx 14 мая 2009 в 12:38

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

VoidEx 14 мая 2009 в 12:27

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, т.е. для типа без элементов список может быть только пустым.

Зарегистрируйтесь на Хабре, чтобы оставить комментарий