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

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

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

Это вообще возможно? А то у меня каша в голове.
lomeo: (лямбда)
Читал статью Bernie Pope "Getting a Fix from the Right Fold" из The Monad. Reader Issue 6. В ней решается задачка о написании dropWhile через foldr. В частности, эта задачка решалась в Graham Hutton "A Tutorial on the Universality and Expressiveness of Fold" через таплы.

У меня удивительно быстро получилось решить эту задачку. Решение было эквивалентным решению 2 в статье.

ExpandПодглядеть )

Profile

lomeo: (Default)
Dmitry Antonyuk

April 2024

S M T W T F S
 123456
7891011 1213
14151617181920
21222324252627
282930    

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

Expand All Cut TagsCollapse All Cut Tags
Page generated Jul. 10th, 2025 03:30 pm
Powered by Dreamwidth Studios