Кстати!

[lomeo]

Для equational reasoning в Haskell можно (иногда нужно) пользоваться GHC Rules (На Haskellwiki), чтобы написанное было читабельным и maintainable, а скомпилированное эффективным. А для нахождения нужных правил можно воспользоваться Theorem for Free. Например, его автоматической выводилкой. Или использовать free / ft команды lambdabot-а.

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

Это я всё мечтаю. Нарисовал нужные типы данных, сформировал по ним типы функций для работы над ними, автоматически построил их реализацию, автоматически построил правила, выбрал нужные для оптимизации. А дальше работаешь легко и непринуждённо. Это идеал, разумеется. Но я уверен, что частично эту работу можно автоматизировать. Типа того, что при доказательстве Coq'ом ему надо указывать стратегии, так же и здесь при реализации тела функции надо направлять "думатель".

Это вообще возможно? А то у меня каша в голове.

Comments

[thesz.livejournal.com]

В самом Хаскеле очень близко к идеалу, но невозможно.

[lomeo.livejournal.com]

Почему? Я не говорю о полностью автоматическом средстве.

[thesz.livejournal.com]

А я думал, что ты именно автоматические средства имел в виду.

В том проекте - модели МИПСа у нас как раз и была такая структура. Сперва сдедали тип, затем в целях улучшения скорости я сперва расставил {-# pragma INLINE #-}, а затем еще и правила подключил.

Особого эффекта, кстати, не дало.

[deni-ok.livejournal.com]

Общий алгоритм для построения всех теорем для произвольных типов? Даже параметризованный хинтами? Хм...

Или достаточно хотя бы каких-то теорем для заданного нового типа + стандартный базис?

Для классических халявных теорем под стандартным базисом я имею ввиду map и его аналог для кортежей

-- У Вадлера это * у функции
map :: (a -> a') -> [a] -> [a']
map f [xs] = [f xs]
-- аналог map для кортежей
(***) :: (a -> a') -> (b -> b') -> (a, b) -> (a', b')
(***) f g (x, y) = (f x, g y)

[lomeo.livejournal.com]

Не, ну я понимаю, что польностью это автоматизировать нельзя :)

Это что то вроде всяких помощников "создать геттеры/сеттеры", "добавить конструктор от суперкласса" в ОО. Какие то шаблонные действия. Плюс попытка помочь при выводе правил. Например, видишь, что в данной композици создаётся промежуточная структура. Попробовать найти способ для elimination исходя из композиции функций. Аналогично тому как мы сами размышляем, когда делаем эту операцию.

[lomeo.livejournal.com]

> Общий алгоритм для построения всех теорем для произвольных типов? Даже параметризованный хинтами? Хм...

Ну правила сами по себе мне не нужны :) Они мне нужны для каких то моих строк кода. Т.е. пишу я "map f . map g", и тут можно автоматически определить, что посередине создаётся временный список. Делается попытка именно для этого случая подыскать (сгенерировать) правило, находится "map (f . g)", где этого списка нет.

Мне почему то кажется, что для таких условий (заранее известное выражение, заданная цель) можно провести переписывание с помощью равенств. Только я не разбираюсь во всех этих term rewriting и автоматических equational proving или как они там называются. Потому и спрашиваю вас, о мудрейшие из проницательнейших!

> Или достаточно хотя бы каких-то теорем для заданного нового типа + стандартный базис?

Для начала хотя бы это. Возможно?

[thesz.livejournal.com]

Давно я так высоко не забирался мыслью. ;)

Даже и сказать-то особо нечего. ;)

Когда я занимался написанием частичных дифференциалов почти в промышленных масштабах (в смысле - много и несколько раз переписывал), у меня возникала мысль о построении генератора упростителей на основе алгоритма Knuth-Bendix. Руки, правда, не дошли.

[lomeo.livejournal.com]

Как я читал, Кнут-Бендикс алгоритм классический, наряду с рядом других. Помимо этих алгоритмов есть масса новых, заточенных на более оптимальное выполнение, правда, кажется, для более конкретных задач/условий. Т.е. вроде бы в этой области все что то делают, а вот практические результаты выливаются в какие то игрушки типа djinn да построителя free theorem для известных типов. Возможно, где-то-кто-то-что-то делает, но я об этом не знаю, собственно про этого кого то и хотел спросить.

Ну и что почитать, конечно :-) С чего начать, чтобы в теме хоть чуть чуть ориентироваться.

[thesz.livejournal.com]

Taste of rewriting systems (http://citeseer.ist.psu.edu/dershowitz93taste.html), автор является соавтором модификации Knut-Bendix (terminating Knuth-Bendix, что ли), которая используется, например, в Maude.

Есть еще http://www.program-transformation.org/

Там не очень много, но есть от чего отталкиваться.

[lomeo.livejournal.com]

Спасибо!

[deni-ok.livejournal.com]

Хрен знает :)

Ну я, ничтожнейший из глупейших, могу поделиться лишь своими убогими мыслишками, скорее всего неправильными. :)

Hugs> :t \f g -> fmap f . fmap g
\f g -> fmap f . fmap g :: Functor a => (b -> c) -> (d -> b) -> a d -> a c
Hugs> :t \f g -> fmap (f . g)
\f g -> fmap (f . g) :: Functor a => (b -> c) -> (d -> b) -> a d -> a c

То что ты пишешь про map - шире, чем просто игры со списками. Это для любого функтора верно и является для него одной из двух аксиом
fmap id == id
fmap (f . g) == fmap f . fmap g

Поэтому про тип, параметризованные другим типом правильный вопрос такой - является ли он функтором? Всякий ли однопараметрический алгебраический тип - функтор?

data X a = ... -- тут любая допустимая хрень

Вот я кажется сформулировал вопрос в который сам всегда утыкаюсь - какие свойства есть у X независимо от того что написано справа?

ЗЫ: это вышел просто поток сознания, а не ответ на твой вопрос :)

[lomeo.livejournal.com]

Это действительно не ответ на мой вопрос, я map то взял в качестве примера :) Тем не менее.

> Всякий ли однопараметрический алгебраический тип - функтор?

В случае negative type (или как они там называются, когда переменная слева от стрелки) вроде не работает:

data X a = X (a -> Int)

Тут не к чему (a -> b) применить, чтобы получить X b.

> какие свойства есть у X независимо от того что написано справа?

Он обладает kind :: * -> *. Это уже что-то для анализа, например, при создании экземпляра класса.

З.Ы. А почему Hugs?

[deni-ok.livejournal.com]

Угу, спасибо.

> З.Ы. А почему Hugs?

За таким компьютером оказался, где только он и есть :)

почитав Вадлера и про ТК на отдыхе в деревне :)

[deni-ok.livejournal.com]

>> Или достаточно хотя бы каких-то теорем для заданного нового типа + стандартный базис?

>Для начала хотя бы это. Возможно?

Вроде да.

Собственно халявные теоремы действительно халявные, как я теперь понял :)

Есть у тебя, скажем, функция с типом f :: forall a. a -> a -> C a -> [a]

Пишешь её два раза

f :: a1 -> C a1 -> [a1]

f :: a2 -> C a2 -> [a2]

Поскольку a живёт под квантором общности, то код f каким бы он ни был, не может зависеть ни от каких свойств типа a. А это даёт магическую parametricity: для любой g:a1 -> a2 (то есть вообще для любой функции!) квадрат коммутативен:

            f
dom f{a1} ------> cod f{a1}
 |                   |
 | g                 | g
 V          f        V
dom f{a2} ------> cod f{a2}

То есть пофиг, что делать: сначала применить f, а потом g на кодомене f, или сначала g над всеми вхождениями a1 в домене f, а потом f над её отображённым в a2 доменом.

Осталось протащить g через параметризованные типы в домене и кодомене и халявная теорема готова:

map g (f x xs) = f (g x) (fmap g xs)

Слева от равенства: верхняя (f x xs), а затем правая (map g) стрелки, map - ибо g в кодомене вытаскиваем из списка.
Справа от равенства: сначала протаскиваем g через параметры (предположим, что C - функтор), а потм применяем f над типом a2.

Если же для C нет instance Functor, то надо как-то курить его конструкторы, это, похоже, должно породить дополнительные условия в халявной теореме.


PS. Я много чего в деревне подоказывал, например, что единственная функция с типом композиции - это композиция :)

Re: почитав Вадлера и про ТК на отдыхе в деревне :)

[lomeo.livejournal.com]

Спасибо, с квадратом действительно понятно. Чувствую, в деревне с ТК хорошо :) В пятницу-субботу тоже поеду на пару недель ;-)

Re: почитав Вадлера и про ТК на отдыхе в деревне :)

[deni-ok.livejournal.com]

Я как понял про квадрат, так сразу всё в голове улеглось! У Вадлера длинно, а на самом деле рисуешь диаграмку - и из неё сразу пишешь теорему.

>Чувствую, в деревне с ТК хорошо :)

В деревне с ТК отлично! ;)
Жалел, что мало статей взял. Зато без компьютера, с ручкой и бумагой, знания в голове оседают гораздо лучше. Я, видимо, ретроград :)

>В пятницу-субботу тоже поеду на пару недель ;-)

А я завтра в Абхазию. ;-)

Re: почитав Вадлера и про ТК на отдыхе в деревне :)

[lomeo.livejournal.com]

А мне наверное не до статей будет. Горы-море. Хотя без Хаскеля не останусь это точно :)

Re: почитав Вадлера и про ТК на отдыхе в деревне :)

[deni-ok.livejournal.com]

>А мне наверное не до статей будет.

Мне, наверное, тоже. Но парочку распечатать стоит. Про запас ;)
Сейчас вот думаю, какие.