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

1. Вы абсолютно правильно понимаете корень проблемы с теорией категорий и computer science: пока этим занимаются алгоритмики, не стоит ожидать большого прогресса. Вот вы написали, что "далеко не все виды теории типов имеют семантику" -- но дело в том, что "семантика" у спецов по computer science и "семантика" у модельеров данных, а также программистов больших программ, основанных на domain-driven design парадигме, и вообще у всех прикладных программистов -- это абсолютно разные семантики. Мне обычно стоит некоторого труда объяснить программистам, что данные -- это про аккуратное отображение мира. И мне кажется, что теория категорий может помочь именно в этом: в работе с множеством разнородных баз знаний, для чего нужно устанавливать мэппинг между этими базами знаний (и определять этот мэппинг каким-то простым механизмом, который, как мне кажется, должен прийти как раз из теории категорий). Ну, и все программисты спотыкаются о "разные логики" -- как я понял, Goguen пытается решить этот вопрос, вводя institutions. Аккуратное представление мира и рассуждения для этого представления. Это совсем не то, что обычно обсуждают программисты на хаскеле. Как сказал А.Г.Кушниренко про добавку моделирования данных к алгоритмике, "в третьем классе, наверное, рано -- но в ВУЗе уже поздно". Сейчас же про эту "семантику данных" (а не семантику программ), включая когнитивную науку и семиотическую составляющую не говорят и в ВУЗе. 2. Я также согласен с вашим выводом, что прогресса можно ожидать не столько "от учёных", сколько от людей, занявшихся дидактикой для теории категорий. Я не думаю, что тут будет какой-то "общественный заказ" (финансирование?) или "специально организованная группа". Группу друзей и единомышленников, даже если они живут в разных городах и работают в разных фирмах, легко назвать "специально организованной группой". Когда я в конце 80-х занимался этой самой школьной информатикой, не было там никакой "специальной организации" и "специально собранной группы людей". Были разные люди, которые понимали важность задачи, и каждый на своём рабочем месте делал, что мог: академики общались с людьми из Политбюро, профессура организовывала студентов, а такие как я им всем помогала -- без какой-либо специальной организации с единым центром. Это вполне возможно сделать и сегодня, в любой предметной области. Нужно просто ставить задачу и решать её. 3. У нас есть некоторые разногласия по отношению к "чистой математике", но я совершенно согласен: путь теории категорий в прикладные области лежит через дизайн курса по преподаванию теории категорий неспециалистам. Сейчас путь познания ТК лежит через обширные области математики, после чего рассказывается о собственно теории категорий. Мне кажется, что есть более простой путь: через диаграммные поначалу, а потом текстовые модельные среды, где решаются задачи теории категорий -- примерно так же, как это происходит с треугольниками в геометрии и роботом в программировании. Да, диаграммные головоломки -- от простых к сложным, с сообщением терминов, позволяющих эти головоломки обсуждать. 300 головоломок -- это примерный объем школьного курса. Мне кажется, что это должен быть ещё школьный курс.