Обновить

Комментарии 36

 на самом деле, в Python есть своя система типов

Шок!

Если же серьёзно, то всё жду поста с рассказом о системах типов от практики, а не от теории. Вроде «вот сложная задача и с формальным подходом к типам её решить на порядок проще, чем без него».

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

Полностью согласен

Для самого простого примера рекомендую посмотреть библиотеку pydantic. Вместо того чтобы парсить на входе json в dict, мы парсим его в типизированную структуру данных, автоматически валидируя. Не нужно будет каждый раз проверять, а точно ли есть такой ключ словаря (для глубокой вложенности это вообще ад) а точно знаем, допускается или не допускается отсутствие элемента, и даже знаем что за тип данных там лежит.

>даже знаем что за тип данных там лежит

Справедливости ради, библиотека запускает неявные конвертации, например, если в json пришла строка, а в модели описан int, то строка конвертируется в int и кладётся в модельку. А вообще да, очень удобная библиотека, там ещё есть автоматическое чтение настроек из переменных окружения.

from pydantic import BaseModel

class MyModel(BaseModel):
value: int # тут таб, но хабр его не отображает

print(MyModel.parse_raw('{"value": "20"}')) -> "value=20"

P.S. Как в этом новомодном интерфейсе набирать комментарии? Где кнопка цитирования? Почему, когда я сделал абзац текстом, я не могу добавить в него пустую строку, вместо этого создаётся новый блок кода?

Чудовищно неявные конвертации, явно говоришь что хочешь на выходе int и получаешь int. Если хочешь чтобы он за тебя угадал поставь тип Any

В Pydantic есть строгие типы без конвертации, вот

АТД действительно отличный подход к описанию практически любой проблемы. После того, как привыкаешь к АТД очень грустно возвращаться к языкам без онных и костылить всякие вспомогательные переменные-флаги, навязывать доп логику на значения null, -1 и т.п.

Но не знаю насколько удобно пользоваться АТД в питоне. Не пробовал, все зависит от того, насколько много надо городить избыточного бойлерплейта, чтобы пользоваться АТД. А по статье это непонятно, пока сам не попробуешь не поймёшь.

Вроде «вот сложная задача и с формальным подходом к типам её решить на порядок проще, чем без него».


Практически любая сложная бизнес-логика. Классический пример — это компиляторы. Если писать входной файл генератора, то проще сначала написать парсер на ocamlyacc, а потом на bison (тот же yacc), чем наоборот. Просто потому, что Ocaml хорошо типизирован, а yacc/bison — нет (он всё передаёт через *void).
Вообще-то компиляторы — полный антипод бизнес-логики. Практически нет ввода-вывода, взаимодействия с человеком, а требования не меняются через день.
Итак, алгебраический тип данных — это такой тип данных, который является композицией других типов. Вот такое незатейливое определение.

data Foo = Bar | Baz

Какие типы я тут скомпозировал?


Или вот из вашего же примера:


Например, тип bool — это двухэлементное множество, которое содержит элементы True и False
Вы объявили тип-сумму с двумя конструкторами данных, используя синтаксис Haskell, если я правильно понимаю. Это больше похоже на простой тип-перечисление (Enum в Python). Думаю, что такой тип эквивалентен:
data Foo = Bar () | Baz ()

т.е. в некотором смысле, это композиция единичных типов.
Или я не прав?

Ну вы в своём примере привели тип bool как множество из True и False. В Haskell этот тип описывается кстати аналогичным образом из моего примера:


data Bool = True | False

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

Это самое простое для понимания определение, как мне кажется. Тип Bool в вашем примере — это специальный случай типа-суммы. Ну и в Haskell все типы данных являются алгебраическими.

Статья интересная, спасибо. Один момент: я сейчас как раз вожусь много с питоном, в основном административные скриптики да и визуализации, поэтому мне не очень понятен сценарий использования. Зачем в принципе навешивать типы на Питон?

Если уж наш проект раздулся до размеро, при которых требуется типизация, не проще ли будет достать из широких штанин тот же самый C# и написать сразу на нем?

Если уж наш проект раздулся до размеро, при которых требуется типизация, не проще ли будет достать из широких штанин тот же самый C# и написать сразу на нем?

Что делать, если проект раздувался постепенно и долго, а теперь для доставания C# нужно переписать не одну сотню kloc, на что начальство категорически не согласно? Так-то конечно лучше сразу писать на подходящем инструменте, но тут вечно все упираются в то, что для точного выбора инструментов нужно сначала формализовать требования, а требования постоянно меняются.

На это дело сейчас народ в CS очень активно работает в поле gradual typing.

Кмк, замена Python'у это не C#, а Ocaml. У меня недописанная статья на эту тему лежит.

Ну вот например я сейчас работаю над высокопроизводительной серверной частью ММО, написаной на питоне. Выкинуть и переписать - бессмысленно, да и разработка на C# или Java выйдет в разы менее продуктивной (если что у меня 10+ лет разработки и на Java и на Python в достаточно крупных проектах и больших компаниях).

Добавлю, что такая типизация ещё отлично помогает IDE с автодополнениями.

То есть от типизации польза примерно такая же как и от typescript для javascript, но без необходимости трансляции и отдельного языка - работать становится гораздо проще и продуктивнее.

Простой пример: есть json с определённой структурой данных. В питоне можно задекларировать это с помощью https://docs.python.org/3/library/typing.html#typing.TypedDict и получить статически типизированный код, который во время исполнения будет работать непосредственно с обычными словарями/списками/строками/числами, прочитанными из json-файла без каких-либо конвертаций. В Java так нельзя - лучшее, что мне там встречалось - это Immutables + Jackson, которые всё равно будут требовать перегенерации кода каждый раз, когда трогаешь исходники. И такие фокусы в них займут сотню строк кода против десятка в питоне.

Спасибо, да, согласен с комментариями выше, часто приходится работать с уже довольно большой кодовой базой, в которой нет аннотаций типов вообще. Но есть возможность файл за файлом, постепенно добавлять аннотации типов и mypy будет их проверять. Это как раз и называется gradual typing, и в этом его главная ценность. Понятно, что если вы пишете какой-то простой скрипт автоматизации, или, например, исследуете данные в Jupyter Notebook, то вам не нужны никакие аннотации. И, конечно, вы можете их не использовать. Но если вы разрабатываете большое приложение, то ценность аннотаций и статических проверок значительно увеличивается. Вот, например, история, как dropbox добавлял аннотации для 4 млн строк кода:
dropbox.tech/application/our-journey-to-type-checking-4-million-lines-of-python
Статическая типизация вообще нужна начиная с некоторого размера программы. Если у вас Notebook (Wolfram/Jupyter), вам часто вообще не нужно, чтобы вся программа была корректна! :-) Достаточно корректности нескольких кусков.
Подобный тип данных называют ненаселенным (uninhabited type), и обычно он используется, чтобы показать невычислимость какого-то выражения, например, брошено исключение, выход из программы, бесконечный цикл, и т.п.

Ненаселённый тип чуть сложнее, чем тут написано. Вообще он показывает любое отрицание.


В Python также есть поддержка такого типа данных:

Костыльная и математически кривая (что, впрочем, похоже, норма для питона):


from typing import NoReturn

def id_mono(x : NoReturn) -> NoReturn:
    return x

даёт


main.py:4: error: Return statement in function which does not return
Found 1 error in 1 file (checked 1 source file)

хотя эта функция абсолютно корректна. Вот вам хаскель-код:


-- ненаселённый тип, нет ни одного конструктора:
data Void

idVoid : Void -> Void
idVoid x = x

На всяких идрисах и агдах будет аналогично.


При этом, похоже, всё захардкожено, и сделать свой собственный NoReturn нельзя, что забавно.

Спасибо, да, согласен, с Haskell на этом поле сложно конкурировать. Не только Python, но и любому другому языку
А что значит?
Вообще он показывает любое отрицание.

Это следствие того, что систему типов можно рассматривать как логику.


Например, если у вас есть функция, которая принимает некое целое число n, некий объект с типом n > 10 (то есть, доказательство, что n больше 10), а также объект с типом n < 10, то эта функция вполне может вернуть ненаселённый тип (потому что вызвать её нельзя — никакое n не может быть одновременно больше и меньше 10).


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


И, собственно, как ложь в логике, эти типы используются в первую очередь для доказательств: имея какое-то значение ненаселённого типа, можно получить значение любого типа (что помогает доказывать, что невозможные случаи действительно невозможны, когда компилятор не видит этого по более базовым причинам). Если вам не нужны доказательства, то вам не нужны и ненаселённые типы, для всех практических применений достаточно аннотаций «эта функция никогда не возвращает управление», и, если честно, вынос это на уровень типов выглядит как карго-культ.


Если смотреть с немножко другой стороны, в хаскеле (который на самом деле совсем не топ с точки зрения типов) вы можете создать выражение типа Void без всяких противоречивых предпосылок, просто написав аналог бесконечного цикла:


bad :: Void
bad = bad

а вот уже всякие там идрисы и агды на это ругнутся:


  |
4 | bad = bad
  | ~~~~~~~~~
Main.bad is possibly not total due to recursive path Main.bad
Спасибо за развернутый ответ, интересно

NoReturn, согласно PEP484, можно использовать только в качестве возвращаемого значения. То что mypy пропускает в аргументе похоже на баг.

Похоже, да, это действительно лучше воспринимать как просто аннотацию, а не как полноценный тип.

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

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

Да, абсолютно верно (ну, с точностью до изоморфизма). Также, как и идентичны все типы, содержащие одно значение, два значения (bool там), и так далее.


а значит зачем нам плодить сущности?

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


Я понимаю, что в других языках механика объявления таких типов существует, но имхо это больше выглядит как костыль для реализации определенных фич языка, а не алгебраически разные сущности.

Почему же костыль? Просто частный случай некой более общей концепции.

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

Так проблема в том, что и в нормальном ООП так никто не делает, это костыли.

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

from abc import abstractmethod, ABC

class Client:
	"""
	Условный класс для объектов, осуществляющих вход
	"""
	pass


class SignInMethod(ABC):
	@abstractmethod
	def sign_in(self, client: Client): ...



class SignInWithEmail(SignInMethod):
	def __init__(self, email: str, password: str):
		self._email = email
		self._password = password

	# override только для заглушкек
	def sign_in(self, client: Client):
		client.sign_in_with_email(
			self._email,
			self._password
		)

Только зачем то нужно передавать Client в SignInMethod. Чтобы открыть дверь, нужно предать замок в ключ и вызвать метод открыть. От такого логического поворота головы коллег могут не выдержать, и начнут лопаться как воздушные шарики.

Это как раз вариант с иерархией классов. Часто тип-сумма (тип Union в Python) является более простой альтернативой. Представьте, например, что нужен не только метод sign_in, а метод log для логирования, и метод save_to_db для сохранения в базу данных. Получится, что абстрактный класс должен определять, а все конкретные классы должны реализовывать и эти новые методы. А если таких методов будет не 3, а 10? Каждый класс в иерархии должен знать как обрабатывать sign_in, как логировать какую-то информацию о себе log, как сохранить в БД save_to_db, и т.п. Скорее всего, понадобится использовать паттерн Visitor, чтобы как-то разделить ответственности, определять новый интерфейс visitor-а и реализации.

client.sign_in_with_email(

У вас sign_in_with_email протекает в два места, соответственно, при добавлении нового метода или изменении старого, надо будет лезть и в код клиента и в код метода логина. Скорее всего рано или поздно кто-то что-то забудет из этого.

Интересный вариант. Как будет развиваться этот подход при добавлении нового метода авторизации?

первым делом подумал про sympy

Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

Минуточку внимания