to Markus, имхо все эти танцы с указанием типа выражения в комментариях решают частично только проблему документирования.
Чтобы в питон добавить типизацию с проверкой типов при компиляции, надо в процессе компиляции эмулировать выполнение кода, это как раз пытается делать pylint, но чтобы проверить типизацию точно, надо вычислить тип каждого выражения.
Например у нас есть функция func1 которая получает в качестве аргумента функцию и вызывает ее внутри. по коду вызова можно вычислить типы параметров этой функции, иногда можно вычислить тип результата, но дальше надо проследить все вызовы func1 и убедится что тип аргумента функции соответствуют вычисленному. А это сложно, учитывая динамическое связывание питона в рантайме:). По сути надо проэмулировать все возможные пути выполнения программы в рантайме.
Насколько мне известно эту задачу пока решили только для функциональных языков ( см например haskel)
Имхо, думаю для структурных или ооп языков с динамическим связыванием (типа python, perl и тд.) проблема проверки типизации настолько трудно разрешима , что ее решать не будут , а пойдут путем добавления возможности явно указывать типы для выражений как например в cython сделали, но это уже расширение языка получается :).
