...и в продакшен!

подвиг мазохиста

Пошел вот сюда: http://vic-gorbatov.livejournal.com/116095.html и прослушал все пять частей доклада и дискуссии некоего Андрея Родина, на тему Ловира, топосной логики и т.п. Родин-то как бы нормально, чуши почти не несёт, Ловира правильно пересказывает. Всё это в статьях и книжках было уже 40 лет назад.

Но в аудитории же никто ни хера не понимает, зато языком почесать, Канта покритиковать, Гегеля помянуть, милое дело.

Вот на хера это всё? Это же канатчикова дача.

И ещё вдруг Воеводского приплетают - "как мне сказал Володя Воеводский..." Да ну ё.

Вот так и в компьютерщине, между прочим, в массовом порядке. "Монада - это такая хитрая штучка, внутре неонка и она жужжит, а если нажать на юнит, то выскочит контент, а ещё можно сплющить - и виноват во всём Гегель (или Гоголь)." Неспособность населения к абстрактному мышлению с успехом заменяется способностью произносить бессвязные речи. Каргокульт, ё.

НТК

Народная теория категорий, через типы.

Категория состоит из типов и функций; каждая функция - из какого-то типа А в какой-то тип Б; имеется композиция функций, имеется тождественная функция. Имеется особый тип, Unit, aka (). Функция из () в тип А называется инстансом типа А.

И понеслась. Функтор F - это отображение, заданное на типах (т.е. для каждого типа X задан какой-то тип F[X]), у которого имеется ещё F.map[A,B]: (A => B) => (F[A] => F[B]).

Мономорфизмы, эпиморфизмы.
Подкатегории, декартовы произведения, пулбаки, пределы, копределы, и т.п., монады.
Категория Клейсли, категория алгебр.
Катаморфизмы и проч.

Декартова замкнутость.

Классификатор подтипов (a.instanceOf[X])

Предпучки, топологии Гротендика, топосная логика, семантика Крипке-Жуаяля.
Модальная логика.

жирара-рейнольдса

Как?