Исправление balsoft, (текущая версия) :
И то, и другое – языки программирования :)
Идрис был приведен в пример как ответ на (возможно риторический) вопрос
Как тебе должно проверяться на этапе компиляции то, что вычисляется во время выполнения например?
Ответ: вот так. То, что у Идриса GC, не меняет того факта что проверять на этапе компиляции то, что вычисляется во время выполнения вполне возможно, вот даже конкретно проверка выхода за границы вектора. Раст это не делает потому что во главу угла ставит совместимость с программистами на C (у которых энтузиазм от изучения зависимых типов очень быстро кончится). Это заметно ещё и по отсутствию HKT, и в целом весьма примитивной системе типов. (Кстати, система типов C++ достаточна для выражения зависимых типов, но там это невыносимо больно в отличие от идриса).
Исходная версия balsoft, :
И то, и другое – языки программирования :)
Идрис был приведен в пример как ответ на (возможно риторический) вопрос
Как тебе должно проверяться на этапе компиляции то, что вычисляется во время выполнения например?
Ответ: вот так. То, что у Идриса GC, не меняет того факта что проверять на этапе компиляции то, что вычисляется во время выполнения вполне возможно, вот даже конкретно проверка выхода за границы вектора. Раст это не делает потому что во главу угла ставит производительность и совместимость с программистами на C (у которых энтузиазм от изучения зависимых типов очень быстро кончится). (Кстати, система типов C++ достаточна для выражения зависимых типов, но там это невыносимо больно в отличие от идриса).