... Мохнатый шмель — на душистый хмель ...

Блин... Еще недавно ехидничал над одним человеком: "А ты не боишься использовать непроверенные алгоритмы? Если ты математически не доказал корректность алгоритма, то он может всю твою программу порушить, будь осторожен!" Это так, съехавшая на почве сессии крыша глюкует иногда :-)

Сейчас написал простейшую программку на Хаскелле, просто для проверки задачи из теории чисел. Провозился полчаса, выявил, что каким-то боком влияет проверка на простоту. Функцию prime я из лени скопипастил из чьего-то исходника: там было какое-то хитрое и шустрое решето. Чье-то, ага.
( Исходник под катом )
Убираю проверку на простоту - все работает. Кривовато, но хотя бы работает как должно. Чудеса в решете, не иначе :-) Закончил тем, что стер к черту хитрое решето и написал тупое, но работающее решето Эратосфена. Все работает. Какого хрена, спрашивается?

Кажется я все-таки понял, что такое Curry-Howard isomorphism. Понял также, что разные системы логики - большой пробел в моих знаниях. Ну это я думаю будет поправлено в ближайший год-два.

Как я понял, это изоморфизм валидных программ (а точнее их type signatures в типизированном лямбда-исчислении) и логических теорем intuitionistic logic (что это такое? как я понял из вики, это некое подмножество классической логики, где доказуемо не все, но многое). Как написано в википедии "proofs are programs".

Не совсем понятно как это можно применять практически, но я предположу, что это применяется для вывода типов (или хотя бы проверки корректности type signatures) в GHC. По идее это позволяет для абстрактного понятия типа применять законы формальной логики. У меня есть подозрение, что CHI сыграл очень важную роль в становлении теории типов.

Во время "задушевной беседы с Гуглом" (ТМ) наткнулся на Girard-Reynolds isomorphism. Говорят, что круто, но туториалов типа "изоморфизм для чайников" я не встретил :-(

Чтобы не забыть запишу сюда полезные ссылки по сабжу:
http://en.wikipedia.org/wiki/Curry-Howard_isomorphism
http://www.haskell.org/pipermail/haskell-cafe/2007-July/028301.html
http://scienceblogs.com/goodmath/2006/09/programs_are_proofs_models_and_1.php
http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism
http://en.wikipedia.org/wiki/Lambda_calculus

Сейчас решаю задачки на Haskell. Падает, сцуко, на Stack Overflow. Кроме как на генерации простых чисел падать больше негде. Раньше я использовал интересный алгоритм генерации, найденный на форуме Project Euler'а, который похоже кэшировал их. Сейчас скачал вроде бы более эффективное решето Аткина. Мда, падать со Stack Overflow стал быстрее :-) Со стэком, расширенным до 128 метров, не падает. Правда виснет :-( Профилер плохо относится к убиванию задач по Ctrl+C. Вот такая засада :-) Но, кажется, начал испытывать долгожданный кайф от таких извращений. Правда пока мало.

Мне вот интересно, что еще с Хаскеллем делать, кроме как задачки решать. Чего б такого сделать, чтобы:

• это было достижимо за несколько месяцев


• это не было бы изобретением велосипеда (ну хотя б чтобы разное количество колес было)


• это было бы кому-то нужно кроме меня.

У меня подозрение, что одно из этих условий нужно вычеркнуть. Только вот какое?

P.S. А еще я понял как писать type signatures к функциям.

Понравились следующие цитаты:

Saying that Java is good because it works on all platforms is like saying anal sex is good because it works on all genders. (Unknown Origin)

Software and cathedrals are much the same - first we build them, then we pray. (Anonymous)

If a million monkeys were typing on computers, one of them will eventually write a Java program. The rest of them will write Perl programs. (Anonymous)

"SQL, Lisp, and Haskell are the only programming languages that I've seen where one spends more time thinking than typing." (Philip Greenspun)

"Haskell is faster than C++, more concise than Perl, more regular than Python, more flexible than Ruby, more typeful than C#, more robust than Java, and has absolutely nothing in common with PHP." (Autrijus Tang)

Testing can only prove the presence of bugs, not their absence. (Edsger Dijkstra)

А еще я сегодня открыл для себя гениальную конструкцию B—tree. Поразительно насколько просто и эффективно.

Читаю HaskellWiki. Медленно осознаю, что нихрена не знаю Хаскелля. Впрочем, я и не сомневался. Этой медитации сильно способствует чужой код, который я нихрена не понимаю, но который работает на порядок, другой быстрее моего. Буду читать дальше...

Итак, я обещался рассказать про такой язык, как Haskell. Я уже давно намеревался его поизучать, но все не находилось то времени, то занятия. Так уж сложилось, что мне сложно, просто читая книгу, чего-то изучать. Но тут благодаря avva нашел такой сайт Project Euler. Решая математические задачки на Haskell'е, я смог преодолеть стартовый барьер в его изучении. Теперь о том, что мне показалось интересным.

В первую очередь, это стиль программирования. В Хаскелле используется декларативный стиль. Это означает, что вводится фактически модель задачи. Программист не фиксируется непосредственно на алгоритме, он строит только модель.

По своему синтаксису Haskell близок к математике. В частности, основной единицей является функция, а синтаксис задания списка срисован с аналогичного из теории множеств. Кроме того, в Хаскелле отсутствуют mutable переменные. А значит невозможно задать цикл, ведь для цикла нужен счетчик, а его реализовать нельзя. Остается рекурсия. Но и её, как ни странно, хватает.

Лично я к такому стилю начал привыкать после разбора чужих решений на Хаскелле. На Project Euler после решения задачи становится доступна форумная ветка по данной задаче. Там народ обменивается решениями. Конечно, для этого необходимо вывернуть мозги. В начале изучения мне приходила в голову аналогия с фоткой Гейтса: "Вот так, через хитрозакрученную жопу, оно и работает". Потом это, впрочем, прошло.

Из доступных реализаций Хаскелля сейчас доступен Hugs (весьма тормозной в работе интерпретатор) и GHC (интерпретатор и компилятор в одном флаконе). Я для себя выбрал GHC, так как скомпилированный exe'шник работает всяко быстрее, чем Hugs. А в решении задач bruteforce'ом это очень и очень актуально.

Вообще Haskell - это очень интересный язык. Лично я освоил только малую часть и не до конца научился писать эффективные функциональные программы. Но я думаю, что с практикой это пройдет.

Для начального изучения я читал Yet Another Haskell Tutorial. Теперь в основном мучаю Google :-)) Еще рекомендую почитать ru_lambda и ru_declarative. В ru_lambda где-то полгода назад avva выкладывал прекрасные руководства для начинающих.

Из того, что я совсем понял в Хаскелле, так это как на нем писать прикладные полезные софтины. Единственное, что я слышал, это веб-сервер на Хаскелле и туториал о привязки Хаскелля к GTK+.

Так или иначе я буду изучать Haskell дальше для чего, в частности, завел соответствующий тэг.