juan_gandhi: (Default)
Today 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.

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.
 
 

juan_gandhi: (Default)
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).

Phillips

May. 28th, 2016 09:39 am
juan_gandhi: (VP)
This morning, at Lambdaconf, Paul suddenly spoke about non-boolean logic, about intuitionism, about categories. An interesting turn of events.

Spiewak

May. 28th, 2016 09:37 am
juan_gandhi: (VP)
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:

type E = Validataion[Error, ?] |: Task |: Base

Composition of functors, eh. Makes the code much more readable.

But in general, his code is way too unreadable.

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

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

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

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

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

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

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

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

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

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

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

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

Да хрен с ним.

Там еще был доклад про алгебру процессов. Ну извините, это какой-то был бред. И на джаве.
juan_gandhi: (VP)
If you plan to attend
If you did not pay yet
I have a discount code (discount=$75)

So let me know if interested

Profile

juan_gandhi: (Default)
juan_gandhi

June 2017

S M T W T F S
     1 2 3
4 5 67 8 9 10
11 12 13 14 15 16 17
18 19 20 21 222324
252627282930 

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 23rd, 2017 12:04 am
Powered by Dreamwidth Studios