Рубрика «системы типов»

Система типов — лучший друг программиста - 1

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

Значение в string не лучший тип для записи адреса электронной почты или страны проживания пользователя. Эти значения заслуживают гораздо более богатых и специализированных типов. Мне нужно, чтобы существовал тип данных EmailAddress, который не может быть null. Мне нужна единая точка входа для создания нового объекта этого типа. Он должен валидироваться и нормализироваться перед возвратом нового значения. Мне нужно, чтобы этот тип данных имел полезные методы наподобие .Domain() или .NonAliasValue(), которые бы возвращали для введённого foo+bar@gmail.com значения gmail.com и foo@gmail.com. Эта полезная функциональность должна быть встроена в эти типы. Это обеспечивает безопасность, помогает предотвращать баги и существенно повышает удобство поддержки.
Читать полностью »

Системы типов — это настоящее безумие.

КДПВ в подражание XKCD

Некоторое время назад я уже отметился здесь со статьёй, в которой пытался разобрать, какие гарантии в compile-time может дать система типов Rust. Кое-какие интересные моменты удалось выловить уже тогда, однако больше всего меня зацепил весьма развёрнутый комментарий, описывающий некоторые вещи, доступные в зависимо-типизированном Idris.
Разумеется, я не мог остаться в стороне. Результат исследований доступен на github, а детальный разбор — под катом.

Читать полностью »

Безразмерный воздушный шар. Утилитарная магия анализа размерностей - 1

На написание этой небольшой заметки меня натолкнула недавно опубликованная на Хабре статья Динамика вертикального полёта летательного аппарата легче воздуха. Захотелось написать комментарий, но он быстро перерос во что-то большее и, как кажется, более полезное.

В оригинальной статье приводится пример расчёта динамики воздушного шара или аэростата в атмосфере. При этом учитываются и сопротивление воздуха и градиенты плотности и температуры атмосферы, так что задача сводится к нетривиальному дифференциальному уравнению, которое благополучно решается численно средствами языка Python. В статье всё хорошо: шар взлетел, остановился, где надо, мы получили и предельную высоту и время подъёма. Потребовалось запустить другой шар, скажем, побольше, нагрузить его поосновательнее, или поменять водород на гелий – не проблема – поменяем параметры в программе и снова всё посчитаем. Программка понятная, линейная, работает, что же можно здесь улучшить, если не усложнять модель?

Можно сделать так, чтобы модель и расчёты стали универсально полезными не для какого-то конкретного шара, а для широкого круга задач. Можно обеспечить оптимальную точность вычислений при численном интегрировании дифференциального уравнения. Можно избавиться от необходимости вручную задавать пределы интегрирования и шаг при расчёте в широком диапазоне параметров. Наконец, можно многое рассказать о динамике полёта нашего шара и без численного решения. И для всего этого служит один давний приём, верный и надёжный, когда-то обязательный при любых расчётах на ЭВМ и до их появления, а сейчас факультативный и часто относимый к магии и искусству – приведение уравнений к безразмерному виду и собственным масштабам. Воспользуюсь задачей о воздухоплавании, как примером и покажу, насколько более осмысленным и изящным становится анализ задачи, при использовании этой техники. А потом объясню почему это может быть важным для программистов, и отчего эта статья попала в хаб «Функциональное программирование».

Читать полностью »


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js