Вот меня заботит длинная дистанция от homotopical теории типов к типам языка программирования, а от них к типам, используемым в моделировании данных — ибо современное программирование построено на системах типов не только внутри языков программирования, но и внешних хранилищах. А внешние хранилища с точки зрения типов начинают с теорий концептов (а не теории типов!)
https://www.iep.utm.edu/concepts/ затем идут в победившую де-факто theory theory
https://www.iep.utm.edu/th-th-co/, затем проходят через разбирательство с foundational ontologies (выражение концептов триплами, или таблицами, или графами отношений — BORO Book,
http://borosolutions.net/sites/default/files/Business%20Objects%20-%20Re-Engineering%20for%20Re-Use%20%282nd%20Ed%20-%20watermarked%20draft%20-%2020050531%29.pdf#page=1&zoom=auto,-22,848), затем обсуждается как разница между реляционными базами данных, графовыми базами данных и всякими вариантами knowledge graphs/semantic networks, и потом как абсолютно внетеорийные "пакеты" доступа из языков программирования с их красивыми типами из всяких теорий типов в базы данных с их чёткой привязкой к концептуальным моделям.
То есть между теориями типов и концептуальным моделированием — огромная дыра, программирование на базах знаний/knowledge graphs, базах данных а хоть и графовых и языках программирования с их красивыми околоматематическими рассуждениями о типов оказываются принципиально разными программированиями, а аспект моделирования мира этими типами в базах данных рассматривается, а в языках программирования вроде как нет. Бардак полный, не хочу так: научите меня типам хорошо один раз, чтобы программировать и моделировать и онтологизировать хорошо — и в языках, и в базах данных. Тем более что вместо баз данных для persistance storage всё чаще и чаще просто выгружают данные из программы дампом прямо во внутренних форматах одним куском, и мы имеем странные вещи в работе с данными типа
https://en.wikipedia.org/wiki/Comparison_of_data-serialization_formats — мимо всяких теорий типов или теорий баз данных.
В общем, моё утверждение я бы повторил: работе с типами программистов не учат. Учат понимать какой-то сленг разработчиков компиляторов, чтобы как-то понимать, что происходит в программе. Это да, но это не учат работать с типами, не учат связи типов с концептами, с разницей между работой с типами в языках программирования и базах данных и базах знаний.
Про вероятностное отнесение к типам, т.е. машинное обучение и типы, вероятностное программирование и типы я уж вообще молчу (задача классификации и все достижения в deep learning — это ж ровно оно!).
Так что ответа для меня в моём вопросе про типы и обучение работе с ними таки нет. Есть ответ про "компиляторные типы и что в головах у разработчиков компиляторов", ответ не про информатику в целом.