![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
(no subject)
May. 27th, 2017 09:20 pmToday was a good day.
At 9AM Paul Phillips was talking about "the axes of abstraction". He mixed in a lot of fantastic stuff, but ended with mentioning Bénabou and profunctors nuclei. These things are "just" fixpoints for a certain comonad generated by a profunctor. In some cases they look pretty cute.
10AM: CARLOS RODRIGUES, CORECURSION, CODATA, AND JUST A LITTLE COMBINATIONAL GAME THEORY. The talk of amazing quality. If you listen to it, and watch slides, you'll remember forever the difference. It's just brilliant.
At 9AM Paul Phillips was talking about "the axes of abstraction". He mixed in a lot of fantastic stuff, but ended with mentioning Bénabou and profunctors nuclei. These things are "just" fixpoints for a certain comonad generated by a profunctor. In some cases they look pretty cute.
10AM: CARLOS RODRIGUES, CORECURSION, CODATA, AND JUST A LITTLE COMBINATIONAL GAME THEORY. The talk of amazing quality. If you listen to it, and watch slides, you'll remember forever the difference. It's just brilliant.
11AM: RÚNAR, ADJUNCTIONS IN EVERYDAY LIFE. See also a book, "Generic Programming with Adjunctions". Runar managed to explain adjunctions to the public in simplest Haskell terms. He only tried to evade answering the questions "how can I build an adjoint". Good for him.
1PM: Adam Warski, "THE ORIGINS OF FREE". Pretty elegantly explained how to build a free monad. A little bit evasive, from math p.o.v, but you know, there are different levels.
2PM: ARSENIY ZHIZHELEV, FLEXIBLE TYPED ONTOLOGY APPLICATIONS. Guys, if you ever exchanged data with Spark/sqldb/json, and the like, using some shitty library... drop everything, see Arseniy's slides, and do what he tells you to do. Just the right solutions for serialization/deserialization/data access.
3:30PM - I gave a talk on Grothendieck topologies, using db schemas, TLA+, Groundhog Day, and more monoids. They enjoyed it. Nobody fell asleep. I'm happy - but totally exhausted.
1PM: Adam Warski, "THE ORIGINS OF FREE". Pretty elegantly explained how to build a free monad. A little bit evasive, from math p.o.v, but you know, there are different levels.
2PM: ARSENIY ZHIZHELEV, FLEXIBLE TYPED ONTOLOGY APPLICATIONS. Guys, if you ever exchanged data with Spark/sqldb/json, and the like, using some shitty library... drop everything, see Arseniy's slides, and do what he tells you to do. Just the right solutions for serialization/deserialization/data access.
3:30PM - I gave a talk on Grothendieck topologies, using db schemas, TLA+, Groundhog Day, and more monoids. They enjoyed it. Nobody fell asleep. I'm happy - but totally exhausted.
my lambda slides
The idea is to show that, well, topology shows us what's distinguishable.
Next year I hope to talk about state machines (the issue is already covered in topos quantum theory, I guess).
The idea is to show that, well, topology shows us what's distinguishable.
Next year I hope to talk about state machines (the issue is already covered in topos quantum theory, I guess).
To compose two monads, you need to provide a Traverse: G[F[G[X]]] → F[G[G[X]]]
Kinda obvious.
He is talking about Emm; something like Eff, for composing monads. Sure need tons of implicits.
I like this notation:
Composition of functors, eh. Makes the code much more readable.
But in general, his code is way too unreadable.
Not enough category theory, too.
Kinda obvious.
He is talking about Emm; something like Eff, for composing monads. Sure need tons of implicits.
I like this notation:
type E = Validataion[Error, ?] |: Task |: BaseComposition of functors, eh. Makes the code much more readable.
But in general, his code is way too unreadable.
Not enough category theory, too.
lambdaconf-2015
May. 23rd, 2015 09:36 pmНу сегодня-то по делу все было. Пол Филипс несравненный выступал в 8:30, а у меня телефон не зарядился (плохой кабель), и я заблудился на 36-й дороге, короче, застал только 10 последних минут. Ну и то. Посмотрите, это все в записи если сейчас нету, так будет. Про совместимость особенно. И вообще. Глубоко копает.
Потом еще Крис Наттикомб классно выступил про параметризацию (нынче все продают бесплатные теоремы); в конце во как сказал: "ну и правильно, что в джаве erasure - это обеспечивает параметричность!"
С утра выступал Гершом из Нью Йорка (который в прошлом году про HoTT задвигал, и который JMacro написал); он тоже про теории, про параметризацию и т.д. Классное было предисловие к моей фигне.
Познакомились, кстати.
Ко мне на лекцию набилось дикое количество народу, на полу сидели. Я их сначала попугал HoTT и топосами, но потом они ржали. А когда кто засыпал, то приходилось вдаваться в подробности; хорошо доска была, там я и рисовал коммутативные диаграммы.
Хорошо вообще пошло.
После лекции подошел один, попросил показать, как экспонента в топосе Гротендика вычисляется. Ну хм, там несложно; главное набрать генераторов, и с ними уже и возиться; если единица и ее подобъекты являются генераторами, то вообще все тривиально; если нет, то чуть менее тривиально, но не сильно. Все через представимые функторы, на самом деле.
Ощущение вот именно что наконец-то воды нам налили.
А кстати, не написать ли что-нибудь на тему вычислений в топосах. Чисто практическое такое - как классификатор сосчитать, как топологии Гротендика перечислить, как импликация вычисляется... Там делов-то несложно.
После меня выступал один интересный парниша, гнал про теорию типов, тоже интуиционистскую, но с точки зрения натурального вывода и т.д. Может, оно с какой-то точки зрения и научнее, но по мне так это все алхимия. Главный вопрос всегда - а почему так? Мне кажется, стандартный ответ на это - "а вот у нас вот так вот". Впрочем, я некомпетентен; но наличие такого аспекта радует; надо будет заняться.
Потом ходил слушал рассказ про скальный проект cats. Так-то впечатляет; типа бросьте вы вашу ненаучную скалази, вот cats все делает правильно и читабельно; я аплодирую обеими руками. Но потом сам себя за руку хватаю. Именно что я заглядывал, и там порядочно тараканов, о которых и разговаривать уже не хочется. Начиная с определения функтора как эндофунктора. Ну и где ваши расширения Кана тогда? Карго культ, что ли... эх. Но все равно, там много хорошего.
Штука только такая, что на приглашение участвовать в нашем категорном семинаре они не реагируют. Так э.
Да хрен с ним.
Там еще был доклад про алгебру процессов. Ну извините, это какой-то был бред. И на джаве.
Потом еще Крис Наттикомб классно выступил про параметризацию (нынче все продают бесплатные теоремы); в конце во как сказал: "ну и правильно, что в джаве erasure - это обеспечивает параметричность!"
С утра выступал Гершом из Нью Йорка (который в прошлом году про HoTT задвигал, и который JMacro написал); он тоже про теории, про параметризацию и т.д. Классное было предисловие к моей фигне.
Познакомились, кстати.
Ко мне на лекцию набилось дикое количество народу, на полу сидели. Я их сначала попугал HoTT и топосами, но потом они ржали. А когда кто засыпал, то приходилось вдаваться в подробности; хорошо доска была, там я и рисовал коммутативные диаграммы.
Хорошо вообще пошло.
После лекции подошел один, попросил показать, как экспонента в топосе Гротендика вычисляется. Ну хм, там несложно; главное набрать генераторов, и с ними уже и возиться; если единица и ее подобъекты являются генераторами, то вообще все тривиально; если нет, то чуть менее тривиально, но не сильно. Все через представимые функторы, на самом деле.
Ощущение вот именно что наконец-то воды нам налили.
А кстати, не написать ли что-нибудь на тему вычислений в топосах. Чисто практическое такое - как классификатор сосчитать, как топологии Гротендика перечислить, как импликация вычисляется... Там делов-то несложно.
После меня выступал один интересный парниша, гнал про теорию типов, тоже интуиционистскую, но с точки зрения натурального вывода и т.д. Может, оно с какой-то точки зрения и научнее, но по мне так это все алхимия. Главный вопрос всегда - а почему так? Мне кажется, стандартный ответ на это - "а вот у нас вот так вот". Впрочем, я некомпетентен; но наличие такого аспекта радует; надо будет заняться.
Потом ходил слушал рассказ про скальный проект cats. Так-то впечатляет; типа бросьте вы вашу ненаучную скалази, вот cats все делает правильно и читабельно; я аплодирую обеими руками. Но потом сам себя за руку хватаю. Именно что я заглядывал, и там порядочно тараканов, о которых и разговаривать уже не хочется. Начиная с определения функтора как эндофунктора. Ну и где ваши расширения Кана тогда? Карго культ, что ли... эх. Но все равно, там много хорошего.
Штука только такая, что на приглашение участвовать в нашем категорном семинаре они не реагируют. Так э.
Да хрен с ним.
Там еще был доклад про алгебру процессов. Ну извините, это какой-то был бред. И на джаве.
lambdaconf-2015
May. 6th, 2015 03:38 pmIf you plan to attend
If you did not pay yet
I have a discount code (discount=$75)
So let me know if interested
If you did not pay yet
I have a discount code (discount=$75)
So let me know if interested
