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

E>Здравствуйте, Roman Odaisky, Вы писали:

E>Этот вопрос к чему относится — нужна ли статическая типизация, или к проблемам вывода типов?

это относится к проблеме проверки типов. не всегда можно вывести все типы в программе, но в рамках системы типов всегда можно проверить корректность выражения.
Единственный способ гарантированной проверки всех типов — подстановка (по аналогии с нормальным порядком вычисления). Такое поддерживается шаблонами в C++, но у шаблонов много других недостатков. Остальные языки пытаются вычислить типы-агрументы функций до проверки корректности типов тела функци (аппликативные вычисления).

Но даже наличие "ленивой" (нормальной) типизации есть теорема Геделя о неполноте, так что можно будет найти корректные выражения, которые невозможно типизировать.