Без заголовка

Самыми близкими к непосредственно программированию оказываются уже упомянутые монады - парадокс с которыми заключается в том, что понятие монады не привязано к отдельной категории, а описывает структуру на произвольной категории, из-за чего ни о какой конкретной категории при объяснении обычно не говорят, и тренировки мышления примерами работы с отдельными категориями нет. В принципе, в качестве категории, от которой мы отталкиваемся при упоминании монад, можно сослаться на какую-то из семантик для подходящей теории типов, это будет реальный, но слишком сложный пример, обычно на него не ссылаются. То есть имеем отсутствие набора простых учебных примеров для тренировки мышления. Как следствие - хотя монада нужна в Хаскелле в точности для возможности один раз воспользоваться алгебраической (по характеру используемых методов) конструкции построения одной категории из другой (“морфизмов с побочным эффектом” из “чистых морфизмов”), этой простой рефлексии я ни в одном monad tutorial-е не увидел. Допустим, я не все читал, но тенденция именно такова. Сомневаюсь, что многие из пишущих отдают себе отчет, что работают в двух категориях, что они отличат эти категории от, например, категории множеств, в которой далеко не все виды теории типов имеют семантику. Как назло, в стандартной библиотеке Хаскелля “функтор” - это не функтор между любыми категориями, а эндофунктор из некоторой фиксированной (но нигде не специфицируемой) категории хаскеллевских типов в себя, что только усугубляет неразбериху в голове новичка. Получается, ситуация в ТК сходна с таковой в алгоритмике, когда ей обучали сразу вычислительным задачам на Фортране или абстрактным преобразованиям на Лиспе в ВУЗах. Когда школьных примеров с программированием простыми командами робота-исполнителя еще не придумали. Но на спуск порога входа до дошкольного возраста в алгоритмике ушло два десятка лет, если я правильно понял, - два десятка лет работы занимающейся этим педагогической группы. Точно так же, ожидать появления “общеобразовательной ТК” без многолетней работы специально организованной для этого группы я бы не стал. Вторым прорывом с алгоритмикой, если я верно понял, был отказ от сложного синтаксиса для школы (и от синтаксиса вообще - для дошкольников). Не знаю, насколько это имеет отношение к ТК. Основные понятия - категория/функтор/естественное преобразование - образуют конкатенативный двумерных синтаксис (т.е. теория 1-категорий может быть аксиоматизирована внутри бикатегории), для которого используется общематематическая нотация термов и равенств, нотация коммутативных диаграмм и альтернативная (дуальная, в определенном смысле) нотация струнных диаграмм. По наблюдениям, специалисты по CS используют общематематическую нотацию, monad-tutorial-щики предпочитают непосредственно ситаксис своего языка программирования. В каком направлении упрощать синтаксис, снижает ли порог входа использование струнных диаграмм (близкое к отказу от синтаксиса) - а приори непонятно и требует исследований на обучаемых. Важен ли конкатенативный синтаксис (без переменных), или проще в понимании трансляция в синтаксис аппликативного языка (с лямбдами) - точно так же трудно сказать (тут практика доказательств подсказывает, что диаграммный поиск удобнее вывода лямбда-выражения по типу, хотя практика программирования заставляет предпочитать переменные для сложных случаев рекурсии). Двумерность же, скорее всего, неустранимый фактор, учитывая высказывание МакЛейна, что категории вводились для возможности работы с естественными преобразованиями. Оптимистическая часть моего вывода отсюда - поставить "деятельность по переформулированию самых разных теорий на промышленную основу" требует постановки задачи по преподаванию ТК неспециальстам, каковую ставить можно и нужно. Пессимистическая - без работы занимающейся именно этим группы результата не будет, а без соцзаказа такая группа не возникнет. Без него - остается надеяться, что всё “вырастет” “как-то само” за неопределенные “лет десять”, как Вы и написали.