Войти
| Системы типов |
|---|
| Общие понятия |
| Основные категории |
|
| Второстепенные категории |
| Смотрите также |
Вывод типа относится к автоматическому определению типа выражения на формальном языке. К ним относятся языки программирования и системы математических типов, а также естественные языки в некоторых областях информатики и лингвистики.
Типы в самом общем виде могут быть связаны с назначенным использованием, предлагая и ограничивая действия, возможные для объекта этого типа. Многие существительные в языке указывают на такое использование. Например, слово поводок указывает на различное применение, чем слово линии. Обозначение чего-либо таблицей указывает на другое обозначение, чем называние его дровами, хотя материально это может быть то же самое. Хотя их материальные свойства делают вещи пригодными для использования в некоторых целях, они также являются предметом определенных обозначений. Это особенно верно в абстрактных областях, а именно в математике и информатике, где материал, наконец, состоит только из битов или формул.
Чтобы исключить нежелательное, но материально возможное использование, концепция типов определяется и применяется во многих вариантах. В математике парадокс Рассела породил первые версии теории типов. В языках программирования типичными примерами являются «ошибки типа», например, приказ компьютеру суммировать значения, которые не являются числами. Хотя это возможно с материальной точки зрения, результат больше не будет значимым и, возможно, пагубным для всего процесса.
В типизации выражение противопоставляется типу. Так, например,, и все отдельные термины с типом для натуральных чисел. Традиционно после выражения следует двоеточие и его тип, например. Это означает, что значение имеет тип. Эта форма также используется для объявления новых имен, например, так же, как введение нового персонажа в сцену словами «детектив Декер».
В отличие от рассказа, в котором обозначения медленно раскрываются, объекты в формальных языках часто должны определяться их типом с самого начала. Кроме того, если выражения неоднозначны, могут потребоваться типы, чтобы сделать предполагаемое использование явным. Например, выражение может иметь тип, но также может читаться как рациональное или действительное число или даже как простой текст.
Как следствие, программы или доказательства могут стать настолько обремененными типами, что желательно вывести их из контекста. Это может быть возможно путем сбора использования нетипизированных выражений (включая неопределенные имена). Если, например, в выражении используется еще не определенное имя n, можно сделать вывод, что n - по крайней мере число. Процесс вывода типа из выражения и его контекста - это вывод типа.
В общем, не только объекты, но и действия имеют типы и могут быть введены просто путем их использования. Для истории из «Звездного пути» таким неизвестным действием может быть «сияние», которое просто выполняется в целях развития сюжета и никогда официально не вводится. Тем не менее, по тому, что происходит, можно определить его тип (транспорт). Кроме того, как объекты, так и действия могут быть построены из их частей. В такой настройке вывод типа не только становится более сложным, но и более полезным, поскольку он позволяет собирать полное описание всего в составной сцене, сохраняя при этом возможность обнаруживать конфликтующие или непреднамеренные использования.
При типизации выражение E противопоставляется типу T, формально записанному как E: T. Обычно типизация имеет смысл только в некотором контексте, который здесь опускается.
В этой обстановке особый интерес представляют следующие вопросы:
Для просто типизированного лямбда-исчисления все три вопроса разрешимы. Не так комфортно положение, когда разрешены более выразительные типы.
Типы - это функция, присутствующая в некоторых языках со строгой статической типизацией. Это часто характерно для языков функционального программирования в целом. Некоторые языки, которые включают вывод типов, включают C ++ 11, C # (начиная с версии 3.0), Chapel, Clean, Crystal, D, F #, FreeBASIC, Go, Haskell, Java (начиная с версии 10), Julia, Kotlin, ML, Nim, OCaml, Opa, RPython, Rust, Scala, Swift, TypeScript, Vala, Dart и Visual Basic (начиная с версии 9.0). Большинство из них используют простую форму вывода типов; система типов Хиндли-Милнера может обеспечить более полный вывод типов. Возможность автоматически выводить типы упрощает многие задачи программирования, позволяя программисту опускать аннотации типов, сохраняя при этом возможность проверки типов.
В некоторых языках программирования все значения имеют тип данных, явно объявленный во время компиляции, ограничивая значения, которые конкретное выражение может принимать во время выполнения. Компиляция «точно в срок» все чаще делает спорным различие между временем выполнения и временем компиляции. Однако исторически сложилось так, что если тип значения известен только во время выполнения, эти языки типизируются динамически. В других языках тип выражения известен только во время компиляции ; эти языки статически типизированы. В большинстве языков со статической типизацией входные и выходные типы функций и локальные переменные обычно должны явно предоставляться аннотациями типов. Например, в C :
int add_one(int x) { int result; /* declare integer result */ result = x + 1; return result; } Подпись этого определения функции, int add_one(int x)заявляет, что add_oneэто функция, которая принимает один аргумент, в целом число и возвращает целое число. int result;объявляет, что локальная переменная resultявляется целым числом. В гипотетическом языке, поддерживающем вывод типов, код может быть написан следующим образом:
add_one(x) { var result; /* inferred-type variable result */ var result2; /* inferred-type variable result #2 */ result = x + 1; result2 = x + 1.0; /* this line won't work (in the proposed language) */ return result; } Это идентично тому, как код пишется на языке Dart, за исключением того, что на него накладываются некоторые дополнительные ограничения, как описано ниже. Можно было бы вывести типы всех переменных во время компиляции. В приведенном выше примере компилятор сделает вывод об этом resultи xимеет целочисленный тип, поскольку константа 1имеет целочисленный тип, и, следовательно, add_oneэто функция int -gt; int. Переменная result2не используется законным образом, поэтому у нее не будет типа.
В воображаемом языке, на котором написан последний пример, компилятор предположит, что при отсутствии информации об обратном, +берет два целых числа и возвращает одно целое число. (Вот как это работает, например, в OCaml. ) Из этого выводчик типа может сделать вывод, что тип x + 1является целым числом, что означает resultцелое число, и, следовательно, возвращаемое значение add_oneявляется целым числом. Точно так же, поскольку +требует, чтобы оба его аргумента были одного типа, он xдолжен быть целым числом и, таким образом, add_oneпринимает одно целое число в качестве аргумента.
Однако в следующей строке result2 вычисляется путем добавления десятичной дроби 1.0с арифметикой с плавающей запятой, что вызывает конфликт при использовании xкак для целочисленных, так и для выражений с плавающей запятой. Правильный алгоритм вывода типов для такой ситуации известен с 1958 года и считается правильным с 1982 года. Он пересматривает предыдущие выводы и с самого начала использует наиболее общий тип: в данном случае с плавающей точкой. Однако это может иметь пагубные последствия, например, использование числа с плавающей запятой с самого начала может вызвать проблемы с точностью, которых не было бы при использовании целочисленного типа.
Однако часто используются вырожденные алгоритмы вывода типов, которые не могут выполнять возврат и вместо этого генерируют сообщение об ошибке в такой ситуации. Такое поведение может быть предпочтительным, поскольку вывод типа не всегда может быть нейтральным с алгоритмической точки зрения, как проиллюстрировано предыдущей проблемой точности с плавающей запятой.
Алгоритм промежуточной общности неявно объявляет result2 как переменную с плавающей запятой, а сложение неявно преобразуется xв переменную с плавающей запятой. Это может быть правильно, если контексты вызова никогда не предоставляют аргумент с плавающей запятой. Такая ситуация показывает разницу между выводом типа, который не включает преобразование типа, и неявным преобразованием типа, которое заставляет данные к другому типу данных, часто без ограничений.
Наконец, существенным недостатком сложного алгоритма вывода типов является то, что результирующее разрешение вывода типов не будет очевидным для людей (особенно из-за обратного отслеживания), что может быть вредным, поскольку код в первую очередь предназначен для понимания людей.
Недавнее появление своевременной компиляции позволяет использовать гибридные подходы, когда тип аргументов, предоставляемых различным контекстом вызова, известен во время компиляции, и может генерировать большое количество скомпилированных версий одной и той же функции. Затем каждую скомпилированную версию можно оптимизировать для другого набора типов. Например, JIT-компиляция позволяет использовать как минимум две скомпилированные версии add_one:
Вывод типа - это способность автоматически выводить, частично или полностью, тип выражения во время компиляции. Компилятор часто может определить тип переменной или сигнатуру типа функции без явных указаний типа. Во многих случаях можно полностью опустить аннотации типов в программе, если система вывода типов достаточно устойчива или программа или язык достаточно просты.
Чтобы получить информацию, необходимую для вывода типа выражения, компилятор либо собирает эту информацию в виде агрегата и последующего сокращения аннотаций типа, заданных для его подвыражений, либо посредством неявного понимания типа различных атомарных значений (например, истина: Bool; 42: целое число; 3,14159: вещественное число и т. Д.). Именно благодаря распознаванию возможного сокращения выражений до неявно типизированных атомарных значений компилятор языка с выводом типа может скомпилировать программу полностью без аннотаций типов.
В сложных формах программирования и полиморфизма высшего порядка компилятор не всегда может сделать такой вывод, и иногда для устранения неоднозначности необходимы аннотации типов. Например, известно, что вывод типа с полиморфной рекурсией неразрешим. Кроме того, явные аннотации типов могут использоваться для оптимизации кода, заставляя компилятор использовать более конкретный (более быстрый / меньший) тип, чем он предполагал.
Некоторые методы вывода типов основаны на теориях удовлетворения ограничений или выполнимости по модулю теорий.
Например, функция Haskell map применяет функцию к каждому элементу списка и может быть определена как:
map f [] = [] map f (first:rest) = f first: map f rest
Определение типа mapфункции происходит следующим образом. mapявляется функцией двух аргументов, поэтому его тип ограничен формой a → b → c. В Haskell шаблоны []и (first:rest)всегда соответствуют спискам, поэтому второй аргумент должен быть типом списка: b = [d]для некоторого типа d. Его первый аргумент fбудет применен к аргументу first, который должен иметь тип d, соответствующий типу в списке аргументах, так f :: d → e( ::средства «имеет типа») для некоторого типа e. map fНаконец, возвращаемое значение - это список того, что fпроизводит, так что [e].
Соединение частей вместе приводит к map :: (d → e) → [d] → [e]. В переменных типа нет ничего особенного, поэтому их можно переименовать как
map:: (a → b) → [a] → [b]
Оказывается, это также самый общий тип, поскольку никакие другие ограничения не применяются. Поскольку вывод типа mapявляется параметрически полиморфный, тип аргументов и результатов fне выводится, а слева, как переменные типа, и поэтому mapмогут быть применены к функциям и списков различных типов, при условии, что фактические типы совпадают в каждом вызове.
Алгоритм, впервые использованный для выполнения вывода типов, теперь неофициально называется алгоритмом Хиндли-Милнера, хотя этот алгоритм следует правильно отнести к Дамасу и Милнеру.
Источником этого алгоритма является алгоритм вывода типов для просто типизированного лямбда-исчисления, который был разработан Хаскеллом Карри и Робертом Фейсом в 1958 году. В 1969 году Дж. Роджер Хиндли расширил эту работу и доказал, что их алгоритм всегда выводит наиболее общий тип. В 1978 году Робин Милнер, независимо от работы Хиндли, при условии, эквивалентный алгоритм, алгоритм W. В 1982 году Луис Дамас окончательно доказал полноту алгоритма Милнера и расширил его для поддержки систем с полиморфными ссылками.
По замыслу, вывод типа, особенно правильный (с возвратом), вводит использование наиболее подходящего общего типа, однако это может иметь последствия, поскольку более общие типы не всегда могут быть алгоритмически нейтральными, типичными случаями являются:
Алгоритмы вывода типов использовались для анализа естественных языков, а также языков программирования. Алгоритмы вывода типов также используются в некоторых грамматических системах индукции и грамматики на основе ограничений для естественных языков.
