История изменений
Исправление AndreyKl, (текущая версия) :
так, на сколько я понимаю, весь смысл зависимых типов в том что есть «возможность применять её (функцию) на этапе компиляции». Т.е. вычислять тип (и правильность типизации) на этапе компиляции в зависимости от значения.
т.е. это как бы не «отдельная тема», а как раз самая что ни на есть суть вопроса.
Исходная версия AndreyKl, :
так, на сколько я понимаю, весь смысл зависимых типов в том что есть «возможность применять её (функцию) на этапе компиляции». Т.е. вычислять тип (и правильность типизации) на этапе компиляции в зависимости от значения.