lambdaconf-2015
May. 23rd, 2015 09:36 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
juan_gandhiНу сегодня-то по делу все было. Пол Филипс несравненный выступал в 8:30, а у меня телефон не зарядился (плохой кабель), и я заблудился на 36-й дороге, короче, застал только 10 последних минут. Ну и то. Посмотрите, это все в записи если сейчас нету, так будет. Про совместимость особенно. И вообще. Глубоко копает.
Потом еще Крис Наттикомб классно выступил про параметризацию (нынче все продают бесплатные теоремы); в конце во как сказал: "ну и правильно, что в джаве erasure - это обеспечивает параметричность!"
С утра выступал Гершом из Нью Йорка (который в прошлом году про HoTT задвигал, и который JMacro написал); он тоже про теории, про параметризацию и т.д. Классное было предисловие к моей фигне.
Познакомились, кстати.
Ко мне на лекцию набилось дикое количество народу, на полу сидели. Я их сначала попугал HoTT и топосами, но потом они ржали. А когда кто засыпал, то приходилось вдаваться в подробности; хорошо доска была, там я и рисовал коммутативные диаграммы.
Хорошо вообще пошло.
После лекции подошел один, попросил показать, как экспонента в топосе Гротендика вычисляется. Ну хм, там несложно; главное набрать генераторов, и с ними уже и возиться; если единица и ее подобъекты являются генераторами, то вообще все тривиально; если нет, то чуть менее тривиально, но не сильно. Все через представимые функторы, на самом деле.
Ощущение вот именно что наконец-то воды нам налили.
А кстати, не написать ли что-нибудь на тему вычислений в топосах. Чисто практическое такое - как классификатор сосчитать, как топологии Гротендика перечислить, как импликация вычисляется... Там делов-то несложно.
После меня выступал один интересный парниша, гнал про теорию типов, тоже интуиционистскую, но с точки зрения натурального вывода и т.д. Может, оно с какой-то точки зрения и научнее, но по мне так это все алхимия. Главный вопрос всегда - а почему так? Мне кажется, стандартный ответ на это - "а вот у нас вот так вот". Впрочем, я некомпетентен; но наличие такого аспекта радует; надо будет заняться.
Потом ходил слушал рассказ про скальный проект cats. Так-то впечатляет; типа бросьте вы вашу ненаучную скалази, вот cats все делает правильно и читабельно; я аплодирую обеими руками. Но потом сам себя за руку хватаю. Именно что я заглядывал, и там порядочно тараканов, о которых и разговаривать уже не хочется. Начиная с определения функтора как эндофунктора. Ну и где ваши расширения Кана тогда? Карго культ, что ли... эх. Но все равно, там много хорошего.
Штука только такая, что на приглашение участвовать в нашем категорном семинаре они не реагируют. Так э.
Да хрен с ним.
Там еще был доклад про алгебру процессов. Ну извините, это какой-то был бред. И на джаве.
Потом еще Крис Наттикомб классно выступил про параметризацию (нынче все продают бесплатные теоремы); в конце во как сказал: "ну и правильно, что в джаве erasure - это обеспечивает параметричность!"
С утра выступал Гершом из Нью Йорка (который в прошлом году про HoTT задвигал, и который JMacro написал); он тоже про теории, про параметризацию и т.д. Классное было предисловие к моей фигне.
Познакомились, кстати.
Ко мне на лекцию набилось дикое количество народу, на полу сидели. Я их сначала попугал HoTT и топосами, но потом они ржали. А когда кто засыпал, то приходилось вдаваться в подробности; хорошо доска была, там я и рисовал коммутативные диаграммы.
Хорошо вообще пошло.
После лекции подошел один, попросил показать, как экспонента в топосе Гротендика вычисляется. Ну хм, там несложно; главное набрать генераторов, и с ними уже и возиться; если единица и ее подобъекты являются генераторами, то вообще все тривиально; если нет, то чуть менее тривиально, но не сильно. Все через представимые функторы, на самом деле.
Ощущение вот именно что наконец-то воды нам налили.
А кстати, не написать ли что-нибудь на тему вычислений в топосах. Чисто практическое такое - как классификатор сосчитать, как топологии Гротендика перечислить, как импликация вычисляется... Там делов-то несложно.
После меня выступал один интересный парниша, гнал про теорию типов, тоже интуиционистскую, но с точки зрения натурального вывода и т.д. Может, оно с какой-то точки зрения и научнее, но по мне так это все алхимия. Главный вопрос всегда - а почему так? Мне кажется, стандартный ответ на это - "а вот у нас вот так вот". Впрочем, я некомпетентен; но наличие такого аспекта радует; надо будет заняться.
Потом ходил слушал рассказ про скальный проект cats. Так-то впечатляет; типа бросьте вы вашу ненаучную скалази, вот cats все делает правильно и читабельно; я аплодирую обеими руками. Но потом сам себя за руку хватаю. Именно что я заглядывал, и там порядочно тараканов, о которых и разговаривать уже не хочется. Начиная с определения функтора как эндофунктора. Ну и где ваши расширения Кана тогда? Карго культ, что ли... эх. Но все равно, там много хорошего.
Штука только такая, что на приглашение участвовать в нашем категорном семинаре они не реагируют. Так э.
Да хрен с ним.
Там еще был доклад про алгебру процессов. Ну извините, это какой-то был бред. И на джаве.
