Pyrefly vs. ty: битва двух Rust-базированных анализаторов типов для Python

[Ktator]

Rust-базированных 🤦‍♂️

Не переживайте — это написал не ИИ

А перевёл, видимо, ИИ, при чём, очень слабенький. Текст на русском читать гораздо сложнее, чем оригинальный английский.

[Tishka17]

Основная идея такова: в корректно типизированной программе удаление аннотации типа не должно приводить к ошибке типов

Это конечно интересная идея, вот только она означает фактически "если линтер не может понять есть тут ошибка или нет, делаем вид что её нет". Вот две коррректно типмзированные программы. Одна с ошибкой, вторая без ошибки типов. Или если угодно, вторая некоррректно типизирована.

x: list[str|int] = []
x.append(1)
x.append("2")

x: list[int] = []
x.append(1)
x.append("2")

И вот если в обеих удалить аннотацию типа, ошибки не добавятся, а наоборот пропадут. То есть линтер перестанет выполнять задачу ради которой его завели - обнаруживать ошибки.

Собственно вы показали код

my_list = [1, "b", None]

В данном случае в качестве типа элементов my_list подойдет любой тип, включающий в себя int, str, NoneType. Во-первых, это тип int|str|NoneType, во-вторых это object, других вариантов я не вижу так как общих родителей у этих типов нет. Я не помню у нас стандарта на то какой из двух вариантов обязан выбрать линтер, поэтому давайте считать что любой из двух подойдет. В целом, я тут даже на стороне mypy - так как у нас ООП язык, мы больше ориентируемся на полиморфизм, чем на произвольные union типы. Лишняя строгость проверок тут как раз позволяет найти больше ошибок, в том числе ошибок дизайна. Если мы считаете что mypy неправильно вывел тип - вы легко можете найти где и проставить его руками. А если если бы он наоборот поступил недостаточно строго, найти ошибочное место было бы сложнее

[cpud47]

Основная идея у такого подхода в том, что ошибка определяется местом потребления. Мотивация в том, что мы хотим выдавать ошибки даже в нетипизированных частях нашей программы.

То есть, пока мы просто создали такой список и не используем — это ок. Но как только мы начинаем его использовать нам тут же обратят внимание, что типы не сходяться(не такие, какие мы ожидали).

Довольно сильный недостаток тоже имеется: ошибки выдаются чаще всего далеко от места их фактического возникновения. Собственно с этим и помогают аннотации типов.

Плюс есть пара теоретических проблем. Для начала, вывод типов в достаточно мощных системах типов, увы, undecidable. Плюс, такого рода задачи зачастую лучше и проще решаются инструментами статического анализа.