Система зависимого от значения типа (или, короче говоря, система зависимого типа) может описывать типы, которые говорят что-то вроде: «Во время оценки (времени выполнения) значение этой переменной всегда будет равно значению этой переменной , который вычисляется с другим процессом оценки ". Автоматическое выведение этого типа из кода влечет за собой автоматическое доказательство теорем. Если набор теорем, которые вы можете выразить, ограничен автоматически доказываемыми, это не будет проблемой, но в случае языков с зависимой типизацией это обычно не так.
Таким образом, у систем с зависимой типизацией не может быть общего (и полного) вывода типа.
Я уверен, что кто-то может дать моральный формальный и полный ответ ...