Feb. 26th, 2013
подвиг мазохиста
Feb. 26th, 2013 02:29 pmПошел вот сюда: 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])
Предпучки, топологии Гротендика, топосная логика, семантика Крипке-Жуаяля.
Модальная логика.
жирара-рейнольдса
Как?
Категория состоит из типов и функций; каждая функция - из какого-то типа А в какой-то тип Б; имеется композиция функций, имеется тождественная функция. Имеется особый тип, Unit, aka (). Функция из () в тип А называется инстансом типа А.
И понеслась. Функтор F - это отображение, заданное на типах (т.е. для каждого типа X задан какой-то тип F[X]), у которого имеется ещё F.map[A,B]: (A => B) => (F[A] => F[B]).
Мономорфизмы, эпиморфизмы.
Подкатегории, декартовы произведения, пулбаки, пределы, копределы, и т.п., монады.
Категория Клейсли, категория алгебр.
Катаморфизмы и проч.
Декартова замкнутость.
Классификатор подтипов (a.instanceOf[X])
Предпучки, топологии Гротендика, топосная логика, семантика Крипке-Жуаяля.
Модальная логика.
жирара-рейнольдса
Как?