Чувствительная к потоку типизация

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

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

Примеры

Цейлон

См. следующий пример на Цейлоне , который иллюстрирует эту концепцию:

// Object? means the variable "name" is of type Object or else null
void hello(Object? name) {
    if (is String name) {
        // "name" now has type String in this block
        print("Hello, ``name``!");
        // and it is possible to call String methods on the variable
        print(" String.size is ``name.size``");
    }
    else if (exists name) {
        // "name" now has type Object in this block
        print("Hello, object ``name``!");
    }
    else {
        print("Hello, world!");
    }
}

          
hello(null);
hello(1);
hello("John Doe");

и что выводит:

Hello, world!
Hello, object 1!
Hello, John Doe!
 String.size is 8

Котлин

См. этот пример в Котлине :

fun hello(obj: Any) {
    // A type cast fails if `obj` is not a String
    obj as String

    // Since the type cast did not fail, `obj` must be a String!
    val l = obj.length

    println("'$obj' is a string of length $l")
}
          
hello("Mooooo")

Преимущества

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

Это также может помочь разработчикам языков предоставлять реализации, которые быстрее выполняют динамические языки за счет статического прогнозирования типа объектов.

Наконец, это повышает безопасность типов и может предотвратить проблемы, связанные с нулевыми указателями. , названная КАР Хоаром — изобретателем нулевых ссылок — «ошибкой на миллиард долларов».

С точки зрения языков программирования разумно сказать, что типизация, чувствительная к потоку, — это функция, которая, наконец, позволила создавать удобные типобезопасные языки программирования с типами объединения и без безудержной динамической проверки. До этого момента попытки добавить эту возможность в такие языки, как Scheme, обычно приводили к непреодолимо большим представлениям типов. Одним из примеров системы с ограниченной поддержкой типов объединения является «Мягкая схема» Райта и Картрайта.

Реализации

Типизированная схема, система типов для Scheme , была первой системой типов с этой функцией. Его преемник, Typed Racket (диалект Racket ), также основан на типизации вхождений. Вскоре после появления Typed Scheme Дэвид Дж. Пирс независимо заново изобрел потоковую типизацию в Whiley .

Типизированный JavaScript заметил, что в «скриптовых» языках потоковая типизация зависит не только от условных предикатов; это также зависит от состояния и потока управления. С тех пор этот стиль был принят в таких языках, как цейлонский , Машинопись и Facebook Flow.

Есть также несколько языков, в которых нет типов объединения , но есть типы, допускающие значение NULL , которые имеют ограниченную форму этой функции, применимую только к типам, допускающим значение NULL, например C# . Котлин , и Лобстер.

Альтернативы

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

См. этот пример макета для Java:

int eval(Node n) {
    return switch(n) {
        // try to type cast "Node" into "IntNode", and create the variable "i" of type "int".
        // If that works, then return the value of "i"
        case IntNode(int i) -> i;
        // try to type cast "Node" into "NegNode", and create the variable "n" of type "Node".
        // If that works, then return the negation of evaluating the "n" node
        case NegNode(Node n) -> -eval(n);
        // try to type cast "Node" into "AddNode", and create the variables "left" and "right" of type "Node".
        // If that works, then return the addition of evaluating the "left" and "right" nodes
        case AddNode(Node left, Node right) -> eval(left) + eval(right);
        // try to type cast "Node" into "MulNode", and create the variables "left" and "right" of type "Node".
        // If that works, then return the multiplication of evaluating the "left" and "right" nodes
        case MulNode(Node left, Node right) -> eval(left) * eval(right);
        // no "default" because the compiler knows all the possible cases have been enumerated
    };
}

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