alogic

На встрече любителей Haskell вчера был просто аншлаг - 6 человек пришло. Ещё должен был быть американец, который из Швеции на велосипеде приехал, но его, видать, в музыкальных тусовках закрутило. Поговорили об архитектурной красоте Haskell, что в других языках надо гвоздями прибивать, здесь можно сделать на уровне библиотеки. Вообще, у Ромы даже презентация появилась (можно смотреть в браузере) про то, что такое объектно-ориентированное программирование с точки зрения Haskell. Выяснилось, что Рома с Женей продолжают разбирать "Mitchell. Foundations for programming languages, 1996 (MIT)" (pdf), причём делают это вдвоём, без оглядки на интеллектуальные меньшинства. Ещё было про стрелки, что в них можно встраивать ограничения, в отличие от монад.

Нью-Йорк пока не собирается переезжать в Одессу, но международный хаскельный турнир Рома Чепляка здесь уже организовал. Хакатон или съезд хакеров для того, чтобы познакомиться и вместе поработать над проектами, написанными на языке Haskell пройдёт 3-5 мая (пятница-воскресенье). Уже заявлены следующие проекты:

• Cabal - установщик хаскелл-программ и библиотек, аналог пакетных менеджеров в дистрибутивах Linux. Один из важнейших инструментов в мире Haskell.
  


• Hakyll - генератор статических сайтов. С помощью него создан сайт Odessa Haskell user group, персональная страница Ивана Веселова.
  


• HasFix - проект Ромы, позволяющий автоматически вносить изменения в исходный код хаскелл-программ, не меняя стиля и форматирования, если разработчики библиотек внесли изменения в API. Достаточно будет вместе с библиотекой прислать файл-описание изменений. Видео-рассказ автора.
  

Одно горе омрачило этот день, пропустил встречу по Haskell. Ну, зато лекция в субботу будет, теперь в 9 утра. Темы и задания по этой же ссылке.

Сегодня Рома Чепляка собирал второй раз любителей Haskell в Одессе (OdHUG). Кроме меня пришёл ещё bodigrim_new и это было прекрасно. Зачем нужна толпа, когда её пока занять нечем? Рома ещё не решил, что он хочет написать такого или сделать, вроде обучающего семинара, чтобы людям было интересно участвовать. А для начала нужна небольшая групка, которая чем-то интересным занята. Остальные наши, в основном слабоинициативные люди, начинают присоединяться потом.

Завтра приезжает Рома Чепляка, чтобы прочесть лекцию "Рекурсивные функции и неподвижные точки". Согласно завету, что "на встречу со звездой надо приходить подготовленными", посмотрел эту страничку. Там в середине сказано, что только Y комбинатор обеспечивает возможность рекурсии. Вот оно что. Помнится Рома уже рассказывал на эту тему год назад, когда мы сидели на траве морского склона, но я тогда не очень понял. Теперь предоставляется второй шанс. А впрочем, что такое год по сравнению с почти столетием, когда Шёнфинкель из Одессы открыл комбинаторную логику.

Поездка в Киев на семинар прошла в напряжённом, но занимательном режиме. Приехав в 7:30, мы, как самые умные, не стали страдать в привокзальных забегаловках, а отъехав пару остановок на троллейбусе, с шиком расположились в пустой, утренней "Пузатой Хате". Потом наша компания, по наводке, рванула на другой конец Киева, чтобы попутешествовать в патентованном трёхмерном кинотеатре IMAX по Международной Космической Станции. Эффект присутствия был просто потрясающий. Ну буквально как будто кинотеатр оказался прямо в космосе. Кино закончилось за 45 минут до начала семинара, так что пришлось двигаться шагом, местами переходящим в бег, чтобы успеть, но мы успели.

На семинар пришло не менее 40 человек. Первым докладчиком был nponeccop, однако он переоценил подготовленность публики и начал со слишком серьёзных результатов, так что пришлось Роме вернуться к азам и провести небольшой ликбез по основам. И он сделал это настолько зажигательно, рассказав про типизированное лямбда-исчисление по Карри, способ вывода термов по Хиндли-Милнеру, что, по-моему, представление об этом получили все, даже если до этого о предмете только слышали. Люди начали активно задавать вопросы, обсуждать и после доклада наградили выступающего заслуженными, бурными аплодисментами.

Завтра очередной раз втроём собираемся на семинар по функциональному программированию, надо хоть упомянуть что было в прошлый раз. Если кратко, то так: eager evaluation, пример по нему, определение универсальной алгебры. Подробности при личной встрече.

UPD. На семинаре была задачка. Доказать, что если на множестве есть некая операция ∘ и существует элемент k такой, что
(k∘x)∘y = x, ∀x,y
то это множество состоит либо из одного, либо из бесконечного количества элементов.

Кратко, что было на семинаре в четверг. Всего нас было трое, так что в основном общались на близкие к основной темы. Начали с понятия подстановки и β-редукции, нормальной формы, то есть такой, когда уже никакие редукции дальше над выражением невозможны, дальше появились понятия слабой и сильной нормализации. Потом решили поупражняться, как же это всё делается руками и разобрали пример.
( пример )
На этом примере иллюстрируется понятие лексического (статического) способа разрешения переменных (lexical scoping), когда значение переменной задаётся ближайшим, самым первым определением. Это отличается от динамического разрешения (dynamic scoping) при котором существуют глобальные переменные и их значение определяется во время выполнения и ближайшим окружением. Это всё связано с понятием замыкания (closure) с помощью которого можно эмулировать объектно-ориентированное программирование.

Сегодня семинарчик открылся по формальным основам программирования. Как и в прошлом году, опять почти про хаскель, но более абстрактно, чтобы лучше понимать что и зачем. Узнал, что есть три вида семантики и существует ужасный парадокс

(\x.F(xx))(\x.F(xx)) = F((\x.F(xx))(\x.F(xx)))

то есть любая функция F должна иметь неподвижную точку (точку, в которой значение функции равно самой этой точке, либо такой же функции, программе, если мы над ними преобразования производим). А это несправедливо по отношению к функции отрицания, например.

Upd. Литература.
Барендрегт X. Ламбда-исчисление.
В частности, конструкции ламбда-исчисления воспитывают интуицию, позволяющую ориентироваться в семантике языков программирования. Эта книга написана для логиков, математиков, специалистов по информатике и философов.

Сегодня присутствовал при том, как рождаются монады. Чистая детская радость от того, что хоть что-то понимаешь:)