Чувствительная к потоку типизация
| Типовые системы |
|---|
| Общие понятия |
| Основные категории |
| Второстепенные категории |
В теории языков программирования типизация с учетом потока (также называемая типизацией потока или типизацией вхождений ) — это система типов , в которой тип выражения зависит от его положения в потоке управления .
В статически типизированных языках тип выражения определяется типами составляющих его подвыражений. Однако при типизации с учетом потока тип выражения может быть обновлен до более конкретного типа, если он следует за операцией, проверяющей его тип. Операции проверки могут включать предикаты типов, императивные обновления и поток управления.
Примеры [ править ]
Цейлон [ править ]
См. следующий пример на Цейлоне , который иллюстрирует эту концепцию:
// Объект? означает, что переменная "name" имеет тип Object или в противном случае null
void hello ( Object ? name ) {
if ( is String name ) {
// "name" теперь имеет тип String в этом блоке
print ( "Hello, ``name`` !" );
// и можно вызывать методы String для переменной
print ( " String.size is ``name.size``" );
}
else if ( exists name ) {
// "name" теперь имеет тип Object в этом блоке
print ( "Привет, объект ``name``!" );
}
else {
print ( «Привет, мир!» );
}
}
привет ( ноль );
привет ( 1 );
привет ( «Джон Доу» );
и что выводит:
Привет, мир! Здравствуйте, объект 1! Привет, Джон Доу! String.size равен 8
Котлин [ править ]
См. этот пример в Котлине :
fun hello ( obj : Any ) {
// Приведение типа завершается неудачей, если `obj` не является строкой
obj as String
// Поскольку приведение типа не завершилось неудачно, `obj` должен быть строкой!
вал л = объект . length
println ( " $ obj ' — это строка длиной $ l " )
}
hello ( "Mooooo" )
Преимущества [ править ]
Этот метод в сочетании с выводом типа уменьшает необходимость написания аннотаций типов для всех переменных или выполнения приведения типов , как это наблюдается в динамических языках , использующих утиную типизацию . Это уменьшает многословие и делает код более кратким, его легче читать и изменять.
Это также может помочь разработчикам языков предоставлять реализации, которые быстрее выполняют динамические языки за счет статического прогнозирования типа объектов. [1]
Наконец, это повышает безопасность типов и может предотвратить проблемы, связанные с нулевыми указателями. [ как? ] , названная КАР Хоаром — изобретателем нулевых ссылок — «ошибкой на миллиард долларов». [2]
С точки зрения языков программирования разумно сказать, что типизация, чувствительная к потоку, — это функция, которая, наконец, позволила создавать удобные типобезопасные языки программирования с типами объединения и без безудержной динамической проверки. До этого момента попытки добавить эту возможность в такие языки, как Scheme, обычно приводили к непреодолимо большим представлениям типов. Одним из примеров системы с ограниченной поддержкой типов объединения является «Мягкая схема» Райта и Картрайта. [3]
Реализации [ править ]
Typed Scheme, система типов для Scheme , была первой системой типов с этой функцией. [4] Его преемник, Typed Racket (диалект Racket ), также основан на типизации вхождений. [5] Вскоре после появления Typed Scheme Дэвид Дж. Пирс независимо заново изобрел потоковую типизацию в Whiley . [6] [7]
Типизированный JavaScript заметил, что в «скриптовых» языках потоковая типизация зависит не только от условных предикатов; это также зависит от состояния и потока управления. [8] С тех пор этот стиль был принят в таких языках, как цейлонский , [9] Машинопись [10] и Facebook Flow. [11]
Есть также несколько языков, в которых нет типов объединения , но есть типы, допускающие значение NULL , которые имеют ограниченную форму этой функции, применимую только к типам, допускающим значение NULL, например C# . [12] Котлин , [13] [14] и Лобстер. [15]
Альтернативы [ править ]
Сопоставление с образцом достигает тех же целей, что и типизация, чувствительная к потоку, а именно: уменьшение многословия и компенсация более краткого кода, его легче читать и изменять. Это достигается другим способом: он позволяет сопоставлять тип структуры и одновременно извлекать из нее данные, объявляя новую переменную. Таким образом, это сокращает церемонию приведения типов и извлечения значений. Сопоставление с образцом лучше всего работает при использовании в сочетании с алгебраическими типами данных, поскольку все случаи могут быть пронумерованы и статически проверены компилятором.
См. этот пример макета для Java: [16]
int eval ( Node n ) {
return switch ( n ) {
// пытаемся ввести приведение "Node" в "IntNode" и создать переменную "i" типа "int".
// Если это работает, то возвращаем значение "i"
case IntNode ( int i ) -> i ;
// попытаемся ввести приведение "Node" в "NegNode" и создать переменную "n" типа "Node".
// Если это работает, то возвращаем отрицание оценки узла "n"
case NegNode ( Node n ) -> - eval ( n );
// попытаемся ввести приведение "Node" в "AddNode" и создать переменные "left" и "right" типа "Node".
// Если это работает, то возвращаем сложение оценки «левого» и «правого» узлов
case AddNode ( Node left , Node right ) -> eval ( left ) + eval ( right );
// попытаемся ввести приведение "Node" в "MulNode" и создать переменные "left" и "right" типа "Node".
// Если это работает, то возвращаем умножение оценки «левого» и «правого» узлов
case MulNode ( Node left , Node right ) -> eval ( left ) * eval ( right );
// нет "по умолчанию", поскольку компилятор знает, что все возможные случаи перечислены
};
}
В статически типизированном языке преимущество сопоставления с образцом перед типизацией, чувствительной к потоку, заключается в том, что тип переменной всегда остается неизменным: он не меняется в зависимости от потока управления. При записи шаблона, который необходимо сопоставить, объявляется новая переменная, которая будет иметь новый тип.
Ссылки [ править ]
- ^ Лукас Эдер (11 декабря 2014 г.). «Неудобная правда о динамической и статической типизации» . blog.jooq.org . Проверено 11 марта 2016 г.
- ^ Тони Хоар (25 августа 2009 г.). «Нулевые ссылки: ошибка на миллиард долларов» . InfoQ.com.
Я называю это своей ошибкой на миллиард долларов. Это было изобретение нулевой ссылки в 1965 году. В то время я разрабатывал первую комплексную систему типов для ссылок на объектно-ориентированном языке ( ALGOL W ). Моя цель состояла в том, чтобы гарантировать, что любое использование ссылок должно быть абсолютно безопасным, с автоматической проверкой, выполняемой компилятором. Но я не смог устоять перед искушением добавить нулевую ссылку просто потому, что это было так легко реализовать. Это привело к бесчисленным ошибкам, уязвимостям и сбоям в системе, которые, вероятно, причинили боль и ущерб на миллиард долларов за последние сорок лет.
- ^ Райт, Эндрю; Картрайт, Роберт (1 января 1997 г.). «Практическая система мягкого типа для схемы» . Транзакции ACM в языках и системах программирования . 19 (1): 87--152. дои : 10.1145/239912.239917 . Проверено 4 мая 2024 г.
- ^ «Проектирование и реализация типизированной схемы | POPL, 2008» . dl.acm.org .
- ^ «Типирование 5 событий» . docs.racket-lang.org .
- ^ Дэвид Дж. Пирс (22 сентября 2010 г.). «О типах, чувствительных к потоку в Whiley» . whiley.org. Архивировано из оригинала 11 марта 2016 года . Проверено 11 марта 2016 г.
- ^ Дэвид Дж. Пирс (8 апреля 2012 г.). «Whiley — Поточная типизация» . whiley.org. Архивировано из оригинала 11 марта 2016 года . Проверено 11 марта 2016 г.
- ^ «Ввод локального управления и состояния с использованием анализа потока» . Проверено 14 ноября 2016 г.
- ^ «Цейлон — Краткое введение — Типобезопасная нулевая и чувствительная к потоку типизация» . ceylon-lang.org . Проверено 11 марта 2016 г.
- ^ Райан Кавано (18 ноября 2014 г.). «Краткий обзор TypeScript 1.4: типы объединения, защита типов и многое другое» . blogs.msdn.microsoft.com . Проверено 11 марта 2016 г.
- ^ Авик Чаудхури; Бэзил Хосмер; Габриэль Леви (18 ноября 2014 г.). «Flow, новая программа проверки статических типов для JavaScript» . code.facebook.com . Проверено 11 марта 2016 г.
- ^ «Проектирование с использованием ссылочных типов, допускающих значение NULL» . docs.microsoft.com .
- ^ «Нулевая безопасность» . kotlinlang.org . Проверено 11 марта 2016 г.
- ^ «Проверка типов и приведение типов» . kotlinlang.org . Проверено 11 марта 2016 г.
- ^ «Система типов лобстеров» . aardappel.github.io .
- ^ Гэвин Бирман и Брайан Гетц (19 сентября 2023 г.). «JEP 441: Сопоставление шаблонов для переключателя» . openjdk.org . Проверено 14 ноября 2023 г.