Обсуждение

потихоньку созревают подходы к мета-программированию с type-level computations http://impredicative.com/ur/ https://leanprover.github.io/ сюда наверное тоже попадает, судя по описанию есть и попроще, без статической проверки типов или там с работой на уровне классов (свойств объектов а не операций над типами) - что-нить типа F-Logic мне думается это и есть направление "практической" онтологической работы, где под "практическим" подразумевается написание кода еще тут интересно направление feature oriented programming, но оно как-то не развивается вобщем помимо тезиса что онтологические сущности - это типы данных в ЯП, нужно еще добавить computations поверх этих типов что не сложно для динамически типизированных языков - но наверное не очень интересно для онтологической работы и сложно для статически типизированных - но зато гораздо круче в каком-то смысле :)

Вот примерно это сейчас начали обсуждать в https://t.me/typeslife (чат этот появился как раз как следствие комментируемого текста).

Зависимые типы -- это всякие вычисления и логика на типах, как это может помочь в деле моделирования мира? По-моему, вы слишком много ожидаете от них...

на текущий момент у зависимых типов всё довольно так себе, для практического использования они не готовы ещё...