знакомый силовик

Только у Славы Рабиновича в голове знакомый силовик сидит, или у многих есть?

Сидит такой знакомый силовик, и подсказывает решения.

Мне кажется, почти у каждого россиянина в голове должен сидеть такой мужичок-силовичок.

А у кого знакомого силовика в голове нету, тот просто лох и ничего не понимает в жизни. Ведь "на самом деле..." ("на самом деле" - это название для той херни, которую россиянину подсказывает внутренний силовичок).

lambdaconf-2015

Ну сегодня-то по делу все было. Пол Филипс несравненный выступал в 8:30, а у меня телефон не зарядился (плохой кабель), и я заблудился на 36-й дороге, короче, застал только 10 последних минут. Ну и то. Посмотрите, это все в записи если сейчас нету, так будет. Про совместимость особенно. И вообще. Глубоко копает.

Потом еще Крис Наттикомб классно выступил про параметризацию (нынче все продают бесплатные теоремы); в конце во как сказал: "ну и правильно, что в джаве erasure - это обеспечивает параметричность!"

С утра выступал Гершом из Нью Йорка (который в прошлом году про HoTT задвигал, и который JMacro написал); он тоже про теории, про параметризацию и т.д. Классное было предисловие к моей фигне.

Познакомились, кстати.

Ко мне на лекцию набилось дикое количество народу, на полу сидели. Я их сначала попугал HoTT и топосами, но потом они ржали. А когда кто засыпал, то приходилось вдаваться в подробности; хорошо доска была, там я и рисовал коммутативные диаграммы.

Хорошо вообще пошло.

После лекции подошел один, попросил показать, как экспонента в топосе Гротендика вычисляется. Ну хм, там несложно; главное набрать генераторов, и с ними уже и возиться; если единица и ее подобъекты являются генераторами, то вообще все тривиально; если нет, то чуть менее тривиально, но не сильно. Все через представимые функторы, на самом деле.

Ощущение вот именно что наконец-то воды нам налили.

А кстати, не написать ли что-нибудь на тему вычислений в топосах. Чисто практическое такое - как классификатор сосчитать, как топологии Гротендика перечислить, как импликация вычисляется... Там делов-то несложно.

После меня выступал один интересный парниша, гнал про теорию типов, тоже интуиционистскую, но с точки зрения натурального вывода и т.д. Может, оно с какой-то точки зрения и научнее, но по мне так это все алхимия. Главный вопрос всегда - а почему так? Мне кажется, стандартный ответ на это - "а вот у нас вот так вот". Впрочем, я некомпетентен; но наличие такого аспекта радует; надо будет заняться.

Потом ходил слушал рассказ про скальный проект cats. Так-то впечатляет; типа бросьте вы вашу ненаучную скалази, вот cats все делает правильно и читабельно; я аплодирую обеими руками. Но потом сам себя за руку хватаю. Именно что я заглядывал, и там порядочно тараканов, о которых и разговаривать уже не хочется. Начиная с определения функтора как эндофунктора. Ну и где ваши расширения Кана тогда? Карго культ, что ли... эх. Но все равно, там много хорошего.

Штука только такая, что на приглашение участвовать в нашем категорном семинаре они не реагируют. Так э.

Да хрен с ним.

Там еще был доклад про алгебру процессов. Ну извините, это какой-то был бред. И на джаве.