По поводу MskHUG.
Возникли у меня по поводу предстоящего
сборища "MskHUG" некоторые сложности.
Сложности не с тем, чтобы приехать.
А с тем, что есть куча глупых дел и думать
про действительно важные важные и нужные,
и что немаловажно, интересные вещи, сложновато.
Я пока не умею "5 минут подумать про категории",
надо как-то посидеть, "раскрутить мозги"...


Насчёт того, что именно рассказывать...
Я считаю, что нельзя сразу рассказывать
про монады и T-алгебры, хотя эти темы
замечательно ложатся на Haskell-программирование.
Нужно рассказывать с самого начала.
В основах есть много мелких непонятностей,
которые заметно тормозят дальнейшее понимание.
Я сужу не только по себе и своему опыту изучения,
такой вывод я сделал после некоторого общения с людьми...

Предположительно, описание не будет привязано
к конкретному языку, но возможно, мелким шрифтом,
будет сделан Haskell-код (или Agda-код?) с комментариями.

Сначала будет дано определение категории, примеры, про то,
как это можно сделать ещё и краткое сравнение с этими же
определениями, но на основе классической логики предикатов.
Обязательно постараюсь побольше примеров, где категорное описание
действительно оправдано и ведёт к упрощению.
Потом некоторые свойства стрелок, (моно-эпи-изо)морфизмы и типа того.
Сразу ввожу понятия функторов, как стрелок между категориями,
раскрываю тему про то, что функтор -- это сложная стрелка,
это уточнение внутренней структуры стрелки (и объекта).
Потом построения в категории, начинаю с (ко)произведений,
тут же можно будет объяснить категорную модель
simply-typed lambda calculus, потом будут
всякие (ко)уравнители и pullback'и, тут надо постараться
и объяснить алгоритм их построения. Это не очень просто.
После этого (ко)пределы и классификатор подобъектов.
Потом рассказать про топосы, как про модель
higher-order-теорий типов, что-ли...
Либо продолжить тему функторов -- категорию функторов,
сопряжённые функторы, связь с пределами...

В одно выступление это не уместить.
Сколько уместится, я не знаю, эта тема для меня самого новая,
и я ни разу не производил целостного и последовательного объяснения.

Несколько сомневаюсь, но хочу рассказывать
про теорию категорий без объектов.
То есть, с присутствием только стрелок
и особых стрелок -- единичных, они
вполне заменяют понятие "объекта".
От этого теория становится чуть проще,
становится меньше сущностей.
Но, повторюсь, я пока не уверен.

Я убеждён, что объяснение всех этих вещей даже и не главное.
Главное -- это показать, что это несложно, что это всё понятные вещи,
чтобы люди смогли дальше самостоятельно читать литературу.
У меня, например, было много мелких непоняток, и разъяснение их
на самом начальном уровне сэкономило бы кучу усилий (и времени).

Кроме того, если понять эти вещи на основе конструктивной логики,
то классическое будет пониматься совсем просто, конечно, если
оно вообще будет востребовано для нужд computer science.

Самое противное, что я не уверен, что успею подготовить ;-(
А без этого ехать как-то ... стрёмно, что-ли...