Бананы, сорок лет одни бананы...

[lomeo]

К чему я так подробно расписывал получение свёртки для розы? Очевидно, что интуитивно получить её можно сразу. Так я обычно и делаю, воспользовавшись методом размерностей, пардон, программированием "от типов". Возможно, так делаете и вы. Я хочу показать главный недостаток этого подхода - он неформален.


Рассуждаем примерно так. Конструктор один - принимаем один параметр, скажем, функцию f.

foldRose :: typeof(f) -> Rose a -> b

Функция f сворачивает нашу структуру, значит, должна иметь тип -> b. У неё должно быть два аргумента, по одному на каждое поле структуры. Первое поле у нас простое, значит первый аргумент имеет тип a. Второе - список роз, розы свёрнуты в b, значит тип [b].

Итого

foldRose :: (a -> [b] -> b) -> Rose a -> b

Поехали дальше. Этот метод - вывод реализации по типу (вспоминаем djinn) - предполагает использование всех аргументов по максимуму. Ну, допустим, что мы отошли от этого правила. Думаем примерно так:

"У нас есть функция типа a -> [b] -> b и нам надо получить b. Значит, нам надо передать в эту функцию два аргумента: один типа a, а другой типа [b] и тогда результат у нас будет нужного нам типа b. Из Rose a мы легко достанем поле типа a, а в качестве [b] мы можем взять и пустой список".

foldRose f (Rose x xs) = f x []

В данном конкретном случае мы можем проверить нашу реализацию с помощью любого из законов катаморфизма. Возьмём самый простой - закон рефлексивности.

foldRose Rose rose == rose

Очевидно, что это не так. В чём же дело? Вспомним, что мы игнорировали правило об использовании всех аргументов и попробуем исправиться. Единственное место, где мы его нарушили - это [] :: [b]. Можем ли мы получить там что то более осмысленное? У нас есть [Rose a], который мы не использовали. И у нас есть возможность получить b из Rose a - это foldRose f :: Rose a -> b. Ну, а [Rose a] -> [b] в этом случае получить не так уж сложно:

map (foldRose f) :: [Rose a] -> [b]

Мы получили значение типа [b], значение типа a было с самого начала. Осталось только объединить всё вместе:

foldRose f (Rose x xs) = f x (map (foldRose f) xs)

Рефлексивность работает.


В данном конкретном случае нам очень сильно помогает Curry-Howard, но он не гарантирует уникальности доказательства (реализации), т.е. этот метод не формализуем. А вот на основе ТК, думаю, можно построить CataEval.

Comments

[jtootf.livejournal.com]

я рассуждал именно так, да. для формального подхода, увы, сильно не хватает знаний :(

[lomeo.livejournal.com]

У меня пока тоже, но я учусь :-)