Вывод типа , иногда называемый реконструкцией типа , [1] : 320 относится к автоматическому определению типа выражения на формальном языке . К ним относятся языки программирования и системы математических типов , а также естественные языки в некоторых отраслях компьютерной науки и лингвистики .
В типизированном языке тип термина определяет, как он может и не может использоваться в этом языке. Например, рассмотрим английский язык и термины, которые могли бы заполнить пробел во фразе «sing _». Термин «a song» имеет певучий тип, поэтому его можно поместить в пробел, чтобы сформировать осмысленную фразу: «sing a song». С другой стороны, термин «a friend» не имеет певучего типа, поэтому «sing a friend» — бессмыслица. В лучшем случае это может быть метафорой; правила изгиба типа являются особенностью поэтического языка.
Тип термина также может влиять на интерпретацию операций, включающих этот термин. Например, «a song» — составной тип, поэтому мы интерпретируем его как вещь, созданную во фразе «write a song». С другой стороны, «a friend» — тип получателя, поэтому мы интерпретируем его как адресата во фразе «write a friend». На обычном языке мы были бы удивлены, если бы «write a song» означало адресовать письмо песне или «write a friend» означало бы набросок друга на бумаге.
Термины с разными типами могут даже относиться к одному и тому же предмету. Например, мы бы интерпретировали «повесить веревку для белья» как использование, а «повесить поводок» — как убирание, хотя в контексте и «веревка для белья», и «поводок» могут относиться к одной и той же веревке, просто в разное время.
Типизация часто используется для предотвращения слишком общего рассмотрения объекта. Например, если система типов рассматривает все числа как одинаковые, то программист, который случайно напишет код, где 4предполагается, что означает «4 секунды», но интерпретируется как «4 метра», не получит предупреждения о своей ошибке, пока это не вызовет проблемы во время выполнения. Включая единицы в систему типов, эти ошибки можно обнаружить гораздо раньше. В качестве другого примера, парадокс Рассела возникает, когда что угодно может быть элементом множества, а любой предикат может определять множество, но более тщательная типизация дает несколько способов разрешения парадокса. Фактически, парадокс Рассела зажег ранние версии теории типов.
Существует несколько способов, с помощью которых термин может получить свой тип:
delay: seconds := 4в его коде, где двоеточие является общепринятым математическим символом для обозначения термина с его типом. То есть, этот оператор не только устанавливает delayзначение 4, но delay: secondsчасть также указывает, что delayтип 's является количеством времени в секундах.Особенно в языках программирования, компьютеру может быть не так много общих фоновых знаний. В явно типизированных языках это означает, что большинство типов должны быть объявлены явно. Вывод типов направлен на облегчение этой нагрузки, освобождая автора от объявления типов, которые компьютер должен иметь возможность вывести из контекста.
В типизации выражение E противопоставляется типу T, формально записываемому как E : T. Обычно типизация имеет смысл только в некотором контексте, который здесь опускается.
В этой связи особый интерес представляют следующие вопросы:
Для простого типизированного лямбда-исчисления все три вопроса разрешимы . Ситуация не столь комфортна, когда допускаются более выразительные типы.
Типы — это функция, присутствующая в некоторых строго статически типизированных языках. Она часто характерна для функциональных языков программирования в целом. Некоторые языки, которые включают вывод типов, включают C23 , [2] C++11 , [3] C# (начиная с версии 3.0), Chapel , Clean , Crystal , D , F# , [4] FreeBASIC , Go , Haskell , Java (начиная с версии 10), Julia , [5] Kotlin , [6] ML , Nim , OCaml , Opa , Q#, RPython , Rust , [7] Scala , [8] Swift , [9] TypeScript , [10] Vala , [11] Dart , [12] и Visual Basic [13] (начиная с версии 9.0). Большинство из них используют простую форму вывода типов; система типов Хиндли–Милнера может обеспечить более полный вывод типов. Возможность автоматического выведения типов упрощает многие задачи программирования, предоставляя программисту свободу пропускать аннотации типов, при этом позволяя выполнять проверку типов.
В некоторых языках программирования все значения имеют тип данных , явно объявленный во время компиляции , ограничивая значения, которые конкретное выражение может принимать во время выполнения . Все чаще компиляция «на лету» стирает различие между временем выполнения и временем компиляции. Однако исторически, если тип значения известен только во время выполнения, эти языки являются динамически типизированными . В других языках тип выражения известен только во время компиляции ; эти языки являются статически типизированными . В большинстве статически типизированных языков входные и выходные типы функций и локальных переменных обычно должны быть явно указаны аннотациями типов. Например, в ANSI C :
int add_one ( int x ) { int result ; /* объявляем целочисленный результат */ результат = x + 1 ; вернуть результат ; } Сигнатура этого определения функции, , объявляет, что это функция, которая принимает один аргумент, целое число , и возвращает целое число. объявляет, что локальная переменная является целым числом. В гипотетическом языке , поддерживающем вывод типа, код может быть записан следующим образом:int add_one(int x)add_oneint result;result
add_one ( x ) { var result ; /* результат переменной выведенного типа */ var result2 ; /* результат переменной выведенного типа #2 */ result = x + 1 ; result2 = x + 1.0 ; /* эта строка не будет работать (на предлагаемом языке) */ return result ; } Это идентично тому, как код пишется на языке Dart , за исключением того, что он подчиняется некоторым дополнительным ограничениям, описанным ниже. Можно было бы вывести типы всех переменных во время компиляции. В приведенном выше примере компилятор вывел бы это resultи xимел бы тип integer, поскольку константа 1имеет тип integer, и, следовательно, это add_oneфункция int -> int. Переменная result2не используется допустимым образом, поэтому у нее не будет типа.
В воображаемом языке, на котором написан последний пример, компилятор предположил бы, что при отсутствии информации об обратном, +берет два целых числа и возвращает одно целое число. (Так это работает, например, в OCaml .) Из этого вывод типа может сделать вывод, что тип x + 1является целым числом, что означает resultявляется целым числом и, таким образом, возвращаемое значение add_oneявляется целым числом. Аналогично, поскольку +требует, чтобы оба его аргумента были одного типа, xдолжны быть целым числом и, таким образом, add_oneпринимает одно целое число в качестве аргумента.
Однако в следующей строке result2 вычисляется путем добавления десятичной дроби к арифметике 1.0с плавающей точкой , что приводит к конфликту при использовании xкак для целочисленных, так и для выражений с плавающей точкой. Правильный алгоритм вывода типа для такой ситуации известен с 1958 года и считается правильным с 1982 года. Он пересматривает предыдущие выводы и использует наиболее общий тип с самого начала: в данном случае с плавающей точкой. Однако это может иметь пагубные последствия, например, использование плавающей точки с самого начала может привести к проблемам с точностью, которых не было бы с целочисленным типом.
Однако часто используются вырожденные алгоритмы вывода типов, которые не могут откатываться назад и вместо этого генерируют сообщение об ошибке в такой ситуации. Такое поведение может быть предпочтительным, поскольку вывод типов не всегда может быть нейтральным алгоритмически, как показано на примере предыдущей проблемы точности с плавающей точкой.
Алгоритм промежуточной общности неявно объявляет result2 как переменную с плавающей точкой, а сложение неявно преобразует ее xв число с плавающей точкой. Это может быть правильно, если вызывающие контексты никогда не предоставляют аргумент с плавающей точкой. Такая ситуация показывает разницу между выводом типа , который не включает преобразование типа , и неявным преобразованием типа , которое принудительно преобразует данные в другой тип данных, часто без ограничений.
Наконец, существенным недостатком сложного алгоритма вывода типов является то, что результирующее разрешение вывода типов не будет очевидным для людей (в частности, из-за возврата), что может иметь пагубные последствия, поскольку код в первую очередь предназначен для понимания людьми.
Недавнее появление компиляции just-in-time допускает гибридные подходы, где тип аргументов, предоставляемых различными вызывающими контекстами, известен во время компиляции и может генерировать большое количество скомпилированных версий одной и той же функции. Каждая скомпилированная версия затем может быть оптимизирована для другого набора типов. Например, компиляция JIT позволяет иметь по крайней мере две скомпилированные версии add_one :
Вывод типа — это способность автоматически выводить, частично или полностью, тип выражения во время компиляции. Компилятор часто может вывести тип переменной или сигнатуру типа функции без явных аннотаций типа. Во многих случаях можно полностью исключить аннотации типа из программы, если система вывода типа достаточно надежна или программа или язык достаточно просты.
Чтобы получить информацию, необходимую для вывода типа выражения, компилятор либо собирает эту информацию в виде совокупности и последующего сокращения аннотаций типов, данных для его подвыражений, либо посредством неявного понимания типа различных атомарных значений (например, true : Bool; 42 : Integer; 3.14159 : Real; и т. д.). Именно посредством распознавания окончательного сокращения выражений до неявно типизированных атомарных значений компилятор для языка вывода типов может полностью скомпилировать программу без аннотаций типов.
В сложных формах программирования высшего порядка и полиморфизма компилятор не всегда может вывести так много, и аннотации типов иногда необходимы для устранения неоднозначности. Например, известно, что вывод типов с полиморфной рекурсией неразрешим. Более того, явные аннотации типов могут использоваться для оптимизации кода, заставляя компилятор использовать более конкретный (быстрый/меньший) тип, чем он вывел. [14]
Некоторые методы вывода типа основаны на удовлетворении ограничений [15] или теориях выполнимости по модулю [16] .
Например, функция Haskellmap применяет функцию к каждому элементу списка и может быть определена как:
карта f [] = [] карта f ( первая : остальная часть ) = f первая : карта f остальная часть (Напомним, что :в Haskell обозначает cons , структурируя головной элемент и хвост списка в больший список или деструктурируя непустой список в его головной элемент и хвост. Он не обозначает «типа», как в математике и в других местах этой статьи; в Haskell вместо этого записывается оператор «типа» ::.)
Вывод типа для mapфункции происходит следующим образом. mapявляется функцией двух аргументов, поэтому ее тип ограничен формой . В Haskell шаблоны и всегда соответствуют спискам, поэтому второй аргумент должен быть типом списка: для некоторого типа . Ее первый аргумент применяется к аргументу , который должен иметь тип , соответствующий типу в аргументе списка, поэтому ( означает «имеет тип») для некоторого типа . Возвращаемое значение , наконец, является списком всего, что производит, поэтому .a -> b -> c[](first:rest)b = [d]dffirstdf :: d -> e::emap ff[e]
Объединение частей приводит к . Ничего особенного в переменных типа нет, поэтому их можно переименовать какmap :: (d -> e) -> [d] -> [e]
карта :: ( а -> б ) -> [ а ] -> [ б ] Оказывается, это также самый общий тип, поскольку не применяются никакие дополнительные ограничения. Поскольку выведенный тип mapявляется параметрически полиморфным , тип аргументов и результатов fне выводится, а остается как переменные типа, и поэтому mapможет применяться к функциям и спискам различных типов, пока фактические типы совпадают в каждом вызове.
Алгоритмы, используемые программами, такими как компиляторы, эквивалентны неформально структурированным рассуждениям выше, но немного более многословны и методичны. Точные детали зависят от выбранного алгоритма вывода (см. следующий раздел для наиболее известного алгоритма), но пример ниже дает общую идею. Мы снова начинаем с определения map:
карта f [] = [] карта f ( первая : остальная часть ) = f первая : карта f остальная часть (Опять же, помните, что :here — это конструктор списков Haskell, а не оператор «of type», который в Haskell пишется ::.)
Сначала мы создаем новые переменные типа для каждого отдельного термина:
αбудет обозначать тип, mapкоторый мы хотим вывести.βобозначим тип fв первом уравнении.[γ]обозначим тип []в левой части первого уравнения.[δ]обозначим тип []в правой части первого уравнения.εобозначим тип fво втором уравнении.ζ -> [ζ] -> [ζ]обозначим тип :в левой части первого уравнения. (Эта закономерность известна из ее определения.)ηобозначает тип first.θобозначает тип rest.ι -> [ι] -> [ι]обозначим тип :в правой части первого уравнения.Затем мы создаем новые переменные типа для подвыражений, построенных из этих терминов, ограничивая соответствующим образом тип вызываемой функции:
κдолжно обозначать тип . Мы приходим к выводу, что где символ «подобный» означает «унифицирует с»; мы говорим, что , тип , должен быть совместим с типом функции, принимающей a и список s и возвращающей a .map f []α ~ β -> [γ] -> κ~αmapβγκλобозначим тип . Приходим к выводу, что .(first:rest)ζ -> [ζ] -> [ζ] ~ η -> θ -> λμобозначим тип . Приходим к выводу, что .map f (first:rest)α ~ ε -> λ -> μνобозначим тип . Приходим к выводу, что .f firstε ~ η -> νξобозначим тип . Приходим к выводу, что .map f restα ~ ε -> θ -> ξοобозначим тип . Приходим к выводу, что .f first : map f restι -> [ι] -> [ι] ~ ν -> ξ -> οМы также ограничиваем левую и правую части каждого уравнения, чтобы они объединялись друг с другом: κ ~ [δ]и μ ~ ο. В целом система объединений для решения имеет вид:
α ~ β -> [γ] -> κζ -> [ζ] -> [ζ] ~ η -> θ -> λα ~ ε -> λ -> με ~ η -> να ~ ε -> θ -> ξι -> [ι] -> [ι] ~ ν -> ξ -> οκ ~ [δ]μ ~ о
Затем мы подставляем до тех пор, пока больше не останется переменных, которые можно будет исключить. Точный порядок не имеет значения; если код проверяет типы, любой порядок приведет к той же окончательной форме. Давайте начнем с подстановки οдля μи [δ]для κ:
α ~ β -> [γ] -> [δ]ζ -> [ζ] -> [ζ] ~ η -> θ -> λα ~ ε -> λ -> οε ~ η -> να ~ ε -> θ -> ξι -> [ι] -> [ι] ~ ν -> ξ -> ο
Подстановка ζвместо η, [ζ]вместо θи λ, ιвместо ν, и [ι]вместо ξи ο, все это возможно, поскольку конструктор типа like является обратимым по своим аргументам:· -> ·
α ~ β -> [γ] -> [δ]α ~ ε -> [ζ] -> [ι]ε ~ ζ -> ι
Заменяем ζ -> ιи εна , сохраняя второе ограничение β -> [γ] -> [δ], αчтобы мы могли восстановиться αв конце:
α ~ (ζ -> ι) -> [ζ] -> [ι]β -> [γ] -> [δ] ~ (ζ -> ι) -> [ζ] -> [ι]
И, наконец, замена (ζ -> ι)на , βа также ζна γи ιна , δпоскольку конструктор типа , подобный этому, является обратимым, исключает все переменные, специфичные для второго ограничения:[·]
α ~ (ζ -> ι) -> [ζ] -> [ι]
Больше никаких замен невозможно, и перемаркировка дает нам то же самое, что мы нашли, не вдаваясь в эти подробности.map :: (a -> b) -> [a] -> [b]
Алгоритм, впервые использованный для выполнения вывода типа, теперь неформально называется алгоритмом Хиндли–Милнера, хотя алгоритм следует отнести к Дамасу и Милнеру. [17] Его также традиционно называют реконструкцией типа . [1] : 320 Если термин хорошо типизирован в соответствии с правилами типизации Хиндли–Милнера, то эти правила генерируют основную типизацию для этого термина. Процесс обнаружения этой основной типизации является процессом «реконструкции».
Происхождение этого алгоритма — алгоритм вывода типа для простого типизированного лямбда-исчисления , разработанный Хаскеллом Карри и Робертом Фейсом в 1958 году. [ требуется ссылка ] В 1969 году Дж. Роджер Хиндли расширил эту работу и доказал, что их алгоритм всегда выводит наиболее общий тип. В 1978 году Робин Милнер [18] независимо от работы Хиндли предоставил эквивалентный алгоритм, алгоритм W. В 1982 году Луис Дамас [17] наконец доказал, что алгоритм Милнера является полным, и расширил его для поддержки систем с полиморфными ссылками.
По замыслу, вывод типа выведет наиболее общий подходящий тип. Однако многие языки, особенно старые языки программирования, имеют несколько ненадежные системы типов, где использование более общих типов не всегда может быть алгоритмически нейтральным. Типичные случаи включают:
+оператор может добавлять целые числа, но может объединять варианты как строки, даже если эти варианты содержат целые числа.Алгоритмы вывода типов использовались для анализа естественных языков , а также языков программирования. [19] [20] [21] Алгоритмы вывода типов также используются в некоторых системах индукции грамматики [22] [23] и грамматике на основе ограничений для естественных языков. [24]