Кстати!

[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 #-}, а затем еще и правила подключил.

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

[lomeo.livejournal.com]

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

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

[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]

Спасибо!