закончился просмотр "Имаджинариума"

Сегодня я устраивал коллективный просмотр "Имаджинариума". Конечно, кинозал у меня небольшой, пять человек едва размещаются (если с удобствами; вповалку и пятнадцать влезут - но нафиг, будут громко разговаривать). Но важно, что большой экран, и что сабвуфер есть. Иным фильмам сабвуфер обязательно.

После Имаджинариума, конечно, "нормальные" фильмы смотреть как-то глупо.

Посмотрели, и расходиться не хотелось; посмотрели все дополнительные материалы, потом трейлеры. Был соблазн поставить второй раз, с комментариями Гиллиама, но решили оставить на следующий раз. Типа через 2 недели опять буду смотреть.

Ещё, наверное, надо уже покупать блюрэй.

hike party

Сегодня в холмах (горами назвать нельзя) накрапывало, но хаскельщик Артур Ч., который на днях покидает нас, уезжая в DC, таки собрал друзей на прощальный турпоход. И мы, встав в кружок, как в "Поисках Жанра" Аксёнова, сначала стали знакомиться, причём индейским пауавным способом. Человек называет своё имя, а потом имя всех предыдущих назвавшихся. Я стоял последним, и мне пришлось запомнить всех. Артур, Иван, Тереса, Лора, Зюбин, Эван, Ларри, Али, Думла, Кришна, Риши, Майк, Алексис, Ник, Анхилан, Влад. Во как. Зато потом шли, можно было ко всем обращаться по имени.

Тропа грязная, залита водой; Эван, композитор (и хаскельщик, и работает в Гугле пишет на джаве), он вообще в резиновых тапочках, пальцы отдельно... а, ему пофиг, он их Хамболт каунти, он в детстве помогал папе сифонить бензин из соседских машин.

Навстречу раз попалась сосредоточенная группа хайкеров, среди которых была и Люба С., сообщившая, что у них хайк на 18 миль. Фигасе. Мы-то мили три, наверное, прочапали. Рассуждали про всякую фигню; народ упорно не хотел признавать poison oak за poison oak. Флаг в руки. Зато, увидев какой-то серый груздь, стали на него с ужасом смотреть, полагая, что это бледная поганка, от одного вида которой можно протянуть ноги.

Народ, конечно, норовил затянуть беседы про хаскель (в частности, я выяснил мнение Ларри про reader monad); потом пришлось объяснить одному товарищу краткую сущность языка Агда.

Краткое описание языка Агда.

Это функциональный язык с зависимыми типами.

Краткое определение зависимых типов.

Вот представь, у тебя в языке тайп чекер различает массив на 10 элементов и массив на 11 элементов. Зависимые типы - это типы, зависящие от конкретных значений. См в википедии лямбда-куб.

Ещё Ларри стал мне впаривать корефлексивные подкатегории. Из его рассказов я так понял, что речь идёт попеременно о Клейсли и об Эйленберга-Мура - что мы как раз в среду мусолили в его присутствии (но он был устамши).

Майк, стартапщик, приставал ко всем с вопросами, what's your technical background. Я ему сказал, что I would not call my background technical. После чего спросил его про его бекграунд - оказался цифровая обработка биологических сигналов. И в его стартапе он этот молоток применяет для анализа html. Html как биологические сигналы. Он там в них выделяет геномы. И за это деньги платят. Назвал ему две конторы, которые, возможно, чем-то похожим занимаются. Похожим на шизофрению из фильма Beautiful mind. Что не делает это дело не beautiful, я сам бы с таким побаловался на досуге... цинизма бы только поменьше.

А потом пошли в гости к Ивану в Пало Альто, пить чай и есть плюшки. У него под диваном оказалась куча раскладных подушек, на которых все и расселись. Хорошая идея. Я, правда, смылся рано, у меня розетка недовставлена была с утра, провода под напряжением торчали на кухне.