Кстати!

[lomeo]

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

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

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

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

Comments

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

[lomeo.livejournal.com]

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

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

[deni-ok.livejournal.com]

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

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

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

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

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

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

[lomeo.livejournal.com]

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

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

[deni-ok.livejournal.com]

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

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