Вывод типа , иногда называемый реконструкцией типа , [1] :320 относится к автоматическому обнаружению типа выражения в формальном языке . К ним относятся языки программирования и системы математических типов , а также естественные языки в некоторых областях информатики и лингвистики .
Типы в самом общем виде могут быть связаны с назначенным использованием, предполагающим и ограничивающим действия, возможные для объекта этого типа. Многие существительные в языке определяют такое использование. Например, слово « поводок» указывает на другое использование, чем слово « линия» . Назвать что-либо столом означает другое обозначение, чем называть это дровами , хотя по сути это может быть одно и то же. Хотя свойства материала позволяют использовать вещи для определенных целей, они также подлежат особым обозначениям. Это особенно актуально в абстрактных областях, а именно в математике и информатике, где материал в конечном итоге представляет собой лишь биты или формулы.
Чтобы исключить нежелательное, но материально возможное использование, концепция типов определяется и применяется во многих вариациях. В математике парадокс Рассела положил начало появлению первых версий теории типов. В языках программирования типичными примерами являются «ошибки типа», например, команда компьютеру суммировать значения, которые не являются числами. Хотя это возможно с материальной точки зрения, результат больше не будет иметь смысла и, возможно, будет катастрофическим для всего процесса.
При типизации выражение противопоставляется типу. Например, , и являются отдельными терминами типа натуральных чисел . Традиционно за выражением следует двоеточие и его тип, например . Это означает, что значение имеет тип . Эта форма также используется для объявления новых имен, например , во многом аналогично представлению нового персонажа в сцене словами «детектив Декер».
В отличие от истории, в которой обозначения разворачиваются медленно, объекты в формальных языках часто приходится с самого начала определять по их типу. Кроме того, если выражения неоднозначны, могут потребоваться типы, чтобы явно указать предполагаемое использование. Например, выражение может иметь тип , но его также можно читать как рациональное или действительное число или даже как обычный текст .
Как следствие, программы или доказательства могут настолько перегрузиться типами, что их желательно выводить из контекста. Это может быть возможно путем сбора данных об использовании нетипизированных выражений (включая неопределенные имена). Если, например, в выражении используется еще неопределенное имя n , можно заключить, что n — это по крайней мере число. Процесс вывода типа из выражения и его контекста — это вывод типа .
В общем, не только объекты, но и действия имеют типы и могут быть введены просто путем их использования. Для истории «Звездного пути» такой неизвестной деятельностью может быть «сияние», которое ради развития сюжета просто выполняется и никогда официально не представлено. Тем не менее, по тому, что происходит, можно определить его тип (транспорт). Кроме того, как объекты, так и действия могут быть построены из их частей. В таких условиях вывод типов не только становится более сложным, но и более полезным, поскольку позволяет собрать полное описание всего в составной сцене, сохраняя при этом возможность обнаруживать конфликтующие или непреднамеренные варианты использования.
При типизации выражение 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 ; /* объявляем целочисленный результат */ результат = х + 1 ; вернуть результат ; } Сигнатура этого определения функции, , объявляет, что это функция, которая принимает один аргумент, целое число , и возвращает целое число. объявляет, что локальная переменная является целым числом. В гипотетическом языке, поддерживающем вывод типов, код мог бы быть написан следующим образом:int add_one(int x)add_oneint result;result
add_one ( x ) { вар результат ; /* переменная выведенного типа result */ var result2 ; /* результат переменной выведенного типа №2 */ результат = х + 1 ; результат2 = х + 1,0 ; /* эта строка не будет работать (на предложенном языке) */ return result ; } Это идентично написанию кода на языке Dart , за исключением того, что на него налагаются некоторые дополнительные ограничения, описанные ниже. Можно было бы определить типы всех переменных во время компиляции. В приведенном выше примере компилятор определил бы это resultи xимел бы целочисленный тип, поскольку константа 1имеет целочисленный тип и, следовательно, add_oneявляется функцией int -> int. Переменная result2не используется законным образом, поэтому у нее не будет типа.
На воображаемом языке, на котором написан последний пример, компилятор предположил бы, что при отсутствии информации об обратном он +принимает два целых числа и возвращает одно целое. (Вот как это работает, например, в OCaml .) Из этого средство вывода типа может сделать вывод, что тип x + 1является целым числом, что означает, что resultоно является целым числом, и, следовательно, возвращаемое значение add_oneявляется целым числом. Аналогично, поскольку +требуется, чтобы оба аргумента были одного типа, он xдолжен быть целым числом и, следовательно, add_oneпринимает одно целое число в качестве аргумента.
Однако в следующей строке result2 вычисляется путем добавления десятичной дроби к арифметике 1.0с плавающей запятой , что приводит к конфликту при использовании xкак для целочисленных выражений, так и для выражений с плавающей запятой. Правильный алгоритм вывода типа для такой ситуации известен с 1958 года, а его корректность известна с 1982 года. Он пересматривает предыдущие выводы и с самого начала использует наиболее общий тип: в данном случае с плавающей запятой. Однако это может иметь пагубные последствия: например, использование чисел с плавающей запятой с самого начала может привести к проблемам с точностью, которых не было бы при использовании целочисленного типа.
Однако часто используются вырожденные алгоритмы вывода типа, которые не могут вернуться назад и вместо этого в такой ситуации генерируют сообщение об ошибке. Такое поведение может быть предпочтительнее, поскольку вывод типа не всегда может быть нейтральным с точки зрения алгоритма, как иллюстрируется предыдущей проблемой точности с плавающей запятой.
Алгоритм промежуточной общности неявно объявляет result2 как переменную с плавающей запятой, и сложение неявно преобразуется xв число с плавающей запятой. Это может быть правильно, если контексты вызова никогда не предоставляют аргумент с плавающей запятой. Такая ситуация показывает разницу между выводом типа , который не предполагает преобразование типа , и неявным преобразованием типа , которое принудительно приводит данные к другому типу данных, часто без ограничений.
Наконец, существенным недостатком сложного алгоритма вывода типа является то, что результирующее разрешение вывода типа не будет очевидным для людей (особенно из-за обратного отслеживания), что может быть вредным, поскольку код в первую очередь предназначен для того, чтобы быть понятным для людей.
Недавнее появление JIT-компиляции позволяет использовать гибридные подходы, при которых тип аргументов, предоставляемых различным контекстом вызова, известен во время компиляции и может генерировать большое количество скомпилированных версий одной и той же функции. Каждую скомпилированную версию затем можно оптимизировать для другого набора типов. Например, JIT-компиляция позволяет иметь как минимум две скомпилированные версии add_one :
Вывод типа — это возможность автоматически определять, частично или полностью, тип выражения во время компиляции. Компилятор часто может определить тип переменной или сигнатуру типа функции без явных аннотаций типа. Во многих случаях можно полностью исключить аннотации типов из программы, если система вывода типов достаточно надежна или программа или язык достаточно просты.
Чтобы получить информацию, необходимую для вывода типа выражения, компилятор либо собирает эту информацию в виде совокупности и последующего сокращения аннотаций типов, заданных для его подвыражений, либо посредством неявного понимания типа различных атомарных значений (например, true: Bool; 42: целое число; 3.14159: вещественное число и т. д.). Именно благодаря распознаванию возможного сведения выражений к неявно типизированным атомарным значениям компилятор языка вывода типов может скомпилировать программу полностью без аннотаций типов.
В сложных формах программирования высшего порядка и полиморфизма компилятор не всегда может сделать такой вывод, и для устранения неоднозначности иногда необходимы аннотации типов. Например, известно, что вывод типа с помощью полиморфной рекурсии неразрешим. Более того, явные аннотации типов могут использоваться для оптимизации кода, заставляя компилятор использовать более конкретный (более быстрый/меньший) тип, чем он предполагал. [14]
Некоторые методы вывода типа основаны на удовлетворении ограничений [15] или теориях выполнимости по модулю . [16]
Например, функция Haskellmap применяет функцию к каждому элементу списка и может быть определена как:
карта f [] = [] карта f ( первый : отдых ) = f первый : карта f отдых Вывод типа функции 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является параметрически полиморфным , тип аргументов и результатов fне выводится, а остается как переменные типа, и поэтому mapможет применяться к функциям и спискам различных типов, пока фактические типы совпадают в каждом вызове. .
Алгоритм, впервые использованный для вывода типа, теперь неофициально называется алгоритмом Хиндли-Милнера, хотя по праву этот алгоритм следует приписать Дамасу и Милнеру. [17] Ее также традиционно называют реконструкцией типа . [1] : 320 Если термин правильно типизирован в соответствии с правилами типизации Хиндли-Милнера, то правила генерируют основную типизацию для термина. Процесс обнаружения этой основной типизации — это процесс «реконструкции».
Происхождением этого алгоритма является алгоритм вывода типа для просто типизированного лямбда-исчисления , который был разработан Хаскеллом Карри и Робертом Фейсом в 1958 году. В 1969 году Дж . Роджер Хиндли расширил эту работу и доказал, что их алгоритм всегда выводит наиболее общий тип. В 1978 году Робин Милнер [ 18] независимо от работы Хиндли предложил эквивалентный алгоритм — алгоритм W. В 1982 году Луис Дамас [17] наконец доказал, что алгоритм Милнера является полным, и расширил его для поддержки систем с полиморфными ссылками.
По замыслу вывод типа, особенно правильный (с обратным отслеживанием) вывод типа, предполагает использование наиболее общего подходящего типа, однако это может иметь последствия, поскольку более общие типы не всегда могут быть алгоритмически нейтральными, типичными случаями являются:
Алгоритмы вывода типов использовались для анализа естественных языков , а также языков программирования. [19] [20] [21] Алгоритмы вывода типа также используются в некоторых грамматических индукциях [22] [23] и грамматических системах на основе ограничений для естественных языков. [24]