Найти тему

Полезность gradual typing в программировании

Давайте поближе познакомимся с фичей gradual typing, которую многие наверняка применяют, но неосознанно. А в ней таится весьма мощный потенциал, это своеобразная склейка между динамически и статически типизированным кодом, потенциально очень перспективная. Впервые она появилась в массовых языках программирования наверное в начале нынешнего века. Сегодня gradual typing активно применяется в разработке проектов компаниями уровня Microsoft и Facebook, которые даже специально разработали по сути свои gradual type systems, что само по себе показатель важности.

Сама по себе фича выглядит примитивно: в динамических языках можно идентификаторам (в основном переменным) при желании указывать их тип. Воспринимается она часто как второстепенная приляпка: кодил-кодил вроде нормально, потом бах — баг выловил, когда строку записываешь в числовую переменную, а потом из неё что-то вычитаешь. Ну ок, теперь поставим ей тип "целое" для страховки. Что тоже конечно никак не поможет, если не используются сторонние инструменты статического анализа кода.

В статических языках ситуация противоположная: замучился писать кучу if-ов для обработки внешнего данного, которое может быть разных типов, хотя семантика везде одинаковая, и забабахал объект в any-переменную в TypeScript или в dynamic-переменную в C# (и потом какой-нибудь особый тип вылетел в рантайме :).

Gradual typing (последовательная, постепенная типизация) вообще двойственна: с одной стороны, это может быть расширение динамических языков элементами статической типизации, с другой стороны, это может быть ослабление системы статической типизации, разрешение не выполнять проверки типов для частей кода например, или явное введение "безтипового" типа.

Например, разработанный Фейсбуком язык Hack, своеобразное улучшение PHP, совмещает в себе статическую и динамическую типизацию, что и называется gradual typing. Хотя, не, корректнее даже сказать, что Hack — это система типов для PHP, а TypeScript (один из лучших в своей сфере, столько теоретического потенциала в него понапихано) — это система типов для JavaScript. Условно говоря, TypeScript для JS — это как MyPy для Python.

Классическая реализация gradual typing такая, что сам язык с динамической типизацией остаётся таким по умолчанию, но есть возможность статических аннотаций типов например, как сделано в Python 3.x или PHP 7. А в статически типизированных языках поддержка gradual typing реализуется, как я выше говорил, с помощью условных any/dynamic. Вот насчёт Java не знаю, кто подскажет?

Проблема в том, что gradual typing в обоих случаях начинает влиять на семантику программы, если в ней имеется хоть какой-то тайпчекинг. И тут сразу возникают десятки весьма глубоких нюансов. Например, корректнее наверное говорить применительно к статическим системам типов, что в них не gradual typing, а type inference — в Kotlin, Rust, C++11...

Пожалуй, самое главное отличие gradual type system от аннотаций типов — что она полная. Если использовать её на всю мощь, то никакие ошибки, связанные с явными конфликтами типов, до рантайма не доберутся, и вылетит программа только на динамической типизации. А вот аннотации типов ничего такого не гарантируют. "Gradual typing replaces the notion of type equality with a new relation called consistency that relates the dynamic type to every other type. The consistency relation is symmetric but not transitive."

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

А вообще gradual typing родилась из весьма крутых разработок наподобие такой: "Contracts for HOF"
https://users.cs.northwestern.edu/~robby/pubs/papers/..
И тут мы добираемся до проектирования, gradual contracts (инвариантным к параметрам), и как нам построить sound (надёжную) систему типов, для чего и нужны подобные контракты, и вот и получается тут, что для любой нетривиальщины в статически типизированных языках становятся очень нужны gradual types, а для динамических языков это просто спасение в плане применимости формальных методов доказательства правильности.

Потому что в вечном споре что лучше статическая или динамическая типизации (при этом, что однозначно есть формальные преимущества у статической типизации), в повседневной прозаической практике мэйстрима статическая типизация даёт всего два бонуса: 1) ловим много мелких тривиальных ошибок на этапе компиляции, и 2) code completion :)

А динамическая типизация очень здорово повышает продуктивность в целом: возьмём примерно схожие по функциональности ORM-ы; Java Hybernate по объёму кода в 10 раз больше, чем питоновский SQLAlchemy.
Сермяга в том, что динамические языки и создавались, и применялись сперва для быстрой реализации проектов среднего размера, однако когда соответствующие проекты набрали большую популярность и выросли до крупных, тут уже и потребовалась статическая типизация, для чего соответствующие статические языки лучше подходят, и поэтому к Python/PHP/... вынужденно были прикручены аннотации типов :)

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

Хорошая gradual type theory (прикладное применение теорката!)
https://arxiv.org/abs/1802.00061
Очень хорошая подборка материалов
http://samth.github.io/gradual-typing-bib/
===

Две области, где gradual typing полезна уже сегодня:

1) Метапрограммирование. В статически типизированных языках крайне трудно сделать код soundly, когда динамически создаём классы или функции (а это постоянно требуется в объектно-реляционнной раскладке например).

3) Тестирование. Всяческие моки удобно и прозрачно реализуются, ну и в целом, вообще можно врать насчёт системы типов :) А в статических языках для mocks и spies придётся очень много помучиться.

Ну и самое важное наверное, что именно за счёт gradual typing сегодня выраженно и достаточно сильно сокращается разрыв между динамическими и статическими языками, и это очень хорошо. Потому что здесь мы подходим к формальной интеграции проектов с сильно разными системами типов.

И надо всё же признать, что динамические языки очень хорошо развиваются, приближаются к полноценной реализации gradual type system, а в плане скорости разработки проектов малого и среднего размера ощутимо обгоняют статические языки.
===

Резюме:

— если вы пишете на статически типизированных языках, то изучите, как в вашем языке реализована gradual typing — но пока ни в коем случае не применяйте :) Если только не будет какого-то теоретического обоснования задачи (например, контракты или метапрограммирование), или для целей тестирования;

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