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

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

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

	Пояснения для тех, кто подзабыл синтаксис
	let ... in expr -- декларации локальных функций/значений для использования в выражении expr f x = ... -- декларация функции f c параметром x f x -- применение функции f к аргументу x (x, y) -- пара (кортеж из двух элементов, возможно, различного типа) id -- функция, возвращающая свой аргумент без изменений [] -- пустой список (id и [] выбраны просто как примеры выражений несовместимого типа) fst -- функция, возвращающая первый элемент пары, тип (a, b) -> a snd -- функция, возвращающая второй элемент пары, тип (a, b) -> b map -- функция, преобразующая функцию над элементами списка в функцию над списками, тип (a -> b) -> ([a] -> [b])

Пропробуйте мысленно убедиться, что это выражение является типобезопасным в том смысле, что оно не пытается выполнять ни над каким значением операций, которые оно не поддерживает (например, не вызывает список как функцию, и не пытается получить компонент кортежа из функции). Что является его результатом?

Ela, будучи в значительной степени динамически типизированным языком, считает это выражение корректным (как можно убедиться здесь). Haskell же отвергает его, как некорректно типизированное, хотя, если оставить в последней строке только foo map, то он может успешно вывести типы. Если же мы оставим только foo bar, то типы не выводятся, хотя всё же можно убедить Haskell в корректности выражения, включив поддержку rank-2 типов, и вручную добавив аннотацию типа для foo.

Вопрос: Есть ли статическая система типов, способная убедиться в типобезопасности приведённого выше выражения (хотя бы с вручную указанными аннотациями)? Если да, то какой тип она назначит функции foo?

Я постепенно склоняюсь к мысли, что язык по умолчанию должен иметь большей частью динамическую типизацию, с минимальными проверками на корректность (например, отвергать такие выражения, как head map или [] id), но позволять вручную указывать произвольные контракты (включая те, которые не выражаются в "обычных" системах типов, например, что функция принимает непустой список положительных целых чисел, не содержащий дубликатов). Компилятор может иметь разные уровни проверки контрактов: начиная от самых быстых, которые могут работать в фоновом режиме в процессе набора кода и помогать IDE показывать правильное автодополнение, до самых тщательных, которые могут запускаться в процессе continuous integration. Сторонние производители могли бы выпускать продукты, реализующие проверку расширенного множества контрактов.