Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Все равно идею не понимаю. Перенести в compile-time логику работы программы... Так ведь, если доводить до предела, можно потребовать в compile-time определение правильной последовательности всех действий программы. А это означает, что эта последовательность должна быть жестко фиксированной и не зависеть от данных — от них зависимость в compile-time не проверишь же...
Сколько еще лет тебе показывать эту ссылку?

In computer science and logic, a dependent type is a type that depends on a value.

http://en.wikipedia.org/wiki/Dependent_type