what they believe

дыбр

Вчера... вчера я где-то в полчетвёртого зафигачил новый парсер, запустил тесты на ночь на стейджинге, и в шестом часу ломанулся опять в город, на, блин, встречу категорщиков. До города-то доехал нормально, но в городе застрял на всяких там улицах. Да затрахало. Последний раз (в этом году). Заявился в офис Прези в 7:15, меня уже искали.

Ну офис ладно, мы проникли в конце концов; нас было шестеро в сумме. В комнате, куда мы пришли, на доске были остатки урока венгерского, и я обнаружил, что ха, на этом-то уровне mindent tudom. Должны были проходить третью главу книжечки Пирса - typed lambdas, categorical style. Ну и чо. Собралось опять половина новых; объясняй им, что за пределы такие... нет, что такое декартово произведение! И что за суммы такие! Короче, протрахались минут сорок с этой ерундой, потом как-то хитростью (без сопряженных функторов) протащили экспоненту.

Тут ещё новенький, Сергей, всё норовил возразить, в русском стиле, мол, нам эти ваши абстракции и даром не нать, у нас всё множества кругом, и можно ограничить дискурс малыми категориями - теория множеств, дескать, и есть основа вычислительных наук. На предложение охарактеризовать Cat было молчание. Я пытался добиться, какая польза вычислениям от аксиомы выбора. потом нарисовал пример неизмеримого подмножества отрезка [0,1]. Молчанье.

Ну ладно. Я уже совсем был почти pissed off. Плюс голодный; обещанной еды Прези не предоставило.

С божией и шахафовой помощью втянулись, наконец, в книжку. Дошли аж до примерно 20-й строки. Потом мне стали объяснять рулеса типовой лямбды; в частности, постоянно фигурировала какая-то гамма. У меня в книжке никакой гаммы не было, и я стал приставать, откуда взялась эта невидимая гамма.

И тут оказалось, что гамма невидима только у меня в книжке, а у остальных в книжке гамма есть. Пришлось мне руками вписывать гамму!

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

Я же как этот стал приябываться к каждому рулесу. Ну типа вот вы говорите, что x имеет тип A × B - а это ж изоморфно B &time; A, так оно имеет и этот тип? Или чо? Или как?

Меня долго убеждали, что тип парсится в процессе валидации фразы, и определяется однозначно, но тут я совсем озверел - как вы нахер определите однозначно, если пределы в категории, как и вообще все сопряженные, определены с точностью до изоморфизма? Это же бред, почему unit имеет тип Unit, а не Unit^Unit × Unit^X?

И тут Шахаф сказал.

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

О блин. Мы вышли на гомотопическую дорожку. Уже Дан Пипони книжку читает, и ещё кто-то там в Гугле. Короче, надо всё бросать и переучиваться заново. Потому что у Пирса в третьей главе булшит. И что, никто не видел? Тьфу.

Ну и вот, и был уже десятый час, и я сказал всё, у меня завтра в 7 класс, пора. Подцепил Мэтью и Шахафа, потому что блин я ценю каждый момент когда можно поговорить с умным человеком, а Шахаф просто блистает. Он скромен до ужаса, но вот с кем бы я работал.

И вот едем мы, я какую-то музычку по радио поставил, и обсуждаем какую-то хрень ну типа как бы нам перекатиться с семинаром в Заливную, желательно в Маунтин Вью (и другого Мэтью ещё притащить - тоже израильтянин); и с Валерией да с Дэном согласовать, чтоб всем удобно было.

И тут Шахаф говорит - а, а кстати, в хаскеле все монады происходят от карриинга.

Чо?! О блин! Вот чо! Это же representable functors! Главное - пределы сохранять.

Перевариваю.

Ну и заодно, к слову, посмотрел как Максим жжет глаголом на киевском fprog:

http://www.youtube.com/watch?v=lJlqQDMpY3I&feature=youtu.be&a

Ну как мы уже поняли, всё не так просто. Но и не так уж запрещено.

ну и к слову пришлось

Поспал я немного, в шесть уже кофе варил, в семь в школе.

Студентов сегодня мало пришло, 13 всего, знают, что тема "необязательная".

Но которые пришли, те о!

Я им впаривал законы де Моргана для случая трёхзначной интуиционистской логики, потом многозначную булеву (помянул и множественные вселенные в качестве примера), потом логику на poset [0,1], со всеми операциями; и ещё делали упражнения из учебника, но с такими вот интуиционистскими логиками. "если a - куб, с достоверностью x, а b - тетраэдр с достоверностью y, ну и т.д. Ничего, доказывается; законы же есть.

Потом постепенно прокрутил строительство алгебр Гейтинга чисто из требований логики (нужно два моноида, дистрибутивность, ограниченность, и соответствие Галуа для коньюнкции.

И все дела.

После урока подошли и попросили дать им ещё домашних заданий - про моноиды.

Да я чо, я и про алгебры Гейтинга могу дать, только я как-то стеснялся пока.