Исправление balsoft, (текущая версия) :
Как тебе должно проверяться на этапе компиляции то, что вычисляется во время выполнения например?
Существуют dependent types, которые позволяют проверять на этапе компиляции то, что будет вычислено во время выполнения. Для примера см. тип Vect в Idris, получение элемента из которого безопасно т.к. язык требует на этапе компиляции доказать, что длина вектора больше чем номер получаемого элемента.
Исходная версия balsoft, :
Как тебе должно проверяться на этапе компиляции то, что вычисляется во время выполнения например?
Существуют dependent types, которые позволяют проверять на этапе компиляции то, что будет вычислено во время выполнения. См. Idris, там есть тип Vec, получение элемента из которого безопасно т.к. язык требует на этапе компиляции доказать, что длина вектора больше чем номер получаемого элемента.