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

N>Я всегда был убеждённым сторонником статической типизации. Но я регулярно сталкиваюсь с тем, что системы типов, хотя и помогают отлавливать многие ошибки, также отвергают вполне безопасный код (впрочем, это хорошо известный теоретический факт).

не следует ли это из того, что для некоторого "универсального" алгоритма вывода типов может потребоваться очень большое количество времени (NP?) на вывод даже в относительно небольших примерах?

N>Взгляните, например, на это выражение (псевдокод, синтаксис Haskell/Ela):
N>

N>let foo f = (f fst, f snd)
N>    bar g = g (id, [])
N>  in (foo bar, foo map)
N>

N>...Что является его результатом?

Не уверен, что понял этот пример, т.к. никогда не писал ни на Haskell/ML, ни на Ela.
Насколько я понял foo bar вернет (bar fst, bar snd) ==> (fst (id, []), snd (id, [])) ==> (id, []), тип — кортеж.
Соответственно foo map ==> map (id, []) ==> [] -> [], видимо тип аргумента этой функции — пустой список.

Результатом, видимо, будет кортеж ((id, []), [] -> []).

Честно говоря, не понимаю в чем тут проблема, если компилятору не пытаться "увидеть" во всех точках вызова foo один и тот же возвращаемый тип, или может я чего-то не понимаю?

Если отвлечься — в Haskell используется алгоритм вывода типов Hindley-Milner, может быть возможно рассмотреть какую-то надстройку над ним, вариант с эвристиками?

N>Я постепенно склоняюсь к мысли, что язык по умолчанию должен иметь большей частью динамическую типизацию...

Рискну предположить, что сходным примером могла бы быть попытка написания программы с использованием статического и динамического языка программирования тесно интегрированных друг с другом на уровне платформы (пример — JVM, Java + Clojure).
Хотя, java, видимо, не является хорошим примером статической типизации.