Автоматическое определение типов выражений в формальных языках.

Введение

Автоматическое определение типа выражения в формальном языке

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

Нетехническое объяснение

Типы в самом общем представлении могут быть связаны с назначением, предполагая и ограничивая возможные действия для объекта данного типа. Многие существительные в языке указывают на такое назначение. Например, слово "поводок" указывает на другое назначение, чем слово "веревка". Называя что-то столом, мы указываем на другое обозначение, чем называя это дровами, хотя материально это может быть одно и то же. Хотя материальные свойства делают вещи пригодными для определенных целей, они также подвержены конкретным обозначениям. Это особенно актуально в абстрактных областях, таких как математика и информатика, где материал в конечном итоге сводится лишь к битам или формулам. Чтобы исключить нежелательные, но материально возможные варианты использования, понятие типов определяется и применяется в различных вариациях. В математике парадокс Рассела послужил толчком к ранним версиям теории типов. В языках программирования типичными примерами являются "ошибки типов", например, команда компьютеру суммировать значения, которые не являются числами. Хотя это и материально возможно, результат перестанет быть осмысленным и, возможно, окажется катастрофическим для всего процесса. В системе типов выражение противопоставляется типу. Например, , , и – все это отдельные термы с типом для натуральных чисел. Традиционно после выражения следует двоеточие и его тип, например, . Это означает, что значение имеет тип . Эта форма также используется для объявления новых имен, например, , что во многом похоже на представление нового персонажа в сцене словами "детектив Декер". В отличие от истории, где обозначения постепенно раскрываются, объекты в формальных языках часто должны быть определены вместе со своим типом с самого начала. Кроме того, если выражения неоднозначны, типы могут потребоваться для уточнения предполагаемого использования. Например, выражение может иметь тип , но также может интерпретироваться как рациональное или действительное число или даже как обычный текст. В результате программы или доказательства могут быть настолько перегружены типами, что становится желательным выводить их из контекста. Это возможно путем сбора информации об использовании нетипизированных выражений (включая неопределенные имена). Если, например, еще не определенное имя n используется в выражении , можно заключить, что n, по крайней мере, является числом. Процесс вывода типа из выражения и его контекста называется выводом типа. В общем случае типы имеют не только объекты, но и действия, и они могут быть введены просто посредством их использования. В истории о "Звёздном пути" такое неизвестное действие может быть "телепортацией", которая ради развития сюжета просто выполняется и никогда формально не представляется. Тем не менее, можно вывести ее тип (транспортировка) по тому, что происходит. Кроме того, как объекты, так и действия могут быть построены из их частей. В такой ситуации вывод типа может стать не только более сложным, но и более полезным, поскольку он позволяет собрать полное описание всего в составной сцене, при этом сохраняя возможность обнаружения конфликтующих или непреднамеренных вариантов использования.

Types in a most general view can be associated to a designated use suggesting and restricting the activities possible for an object of that type. Many nouns in language specify such uses. For instance, the word leash indicates a different use than the word line. Calling something a table indicates another designation than calling it firewood, though it might be materially the same thing. While their material properties make things usable for some purposes, they are also subject of particular designations. This is especially the case in abstract fields, namely mathematics and computer science, where the material is finally only bits or formulas. To exclude unwanted, but materially possible uses, the concept of types is defined and applied in many variations. In mathematics, Russell's paradox sparked early versions of type theory. In programming languages, typical examples are "type errors", e. g. ordering a computer to sum values that are not numbers. While materially possible, the result would no longer be meaningful and perhaps disastrous for the overall process. In a typing, an expression is opposed to a type. For example, , , and are all separate terms with the type for natural numbers. Traditionally, the expression is followed by a colon and its type, such as This means that the value is of type This form is also used to declare new names, e. g. , much like introducing a new character to a scene by the words "detective Decker". Contrary to a story, where the designations slowly unfold, the objects in formal languages often have to be defined with their type from very beginning. Additionally, if the expressions are ambiguous, types may be needed to make the intended use explicit. For instance, the expression might have a type but could also be read as a rational or real number or even as a plain text. As a consequence, programs or proofs can become so encumbered with types, that it is desirable to deduce them from the context. This can be possible by collecting the uses of untyped expression (including undefined names). If, for instance, a yet undefined name n is used in an expression , one could conclude, that n is at least a number. The process of deducing the type from an expression and its context is type inference. In general not only objects, but also activities have types and may be introduced simply by their use. For a Star Trek story, such an unknown activity could be "beaming", which for sake of the story's flow is just executed and never formally introduced. Nevertheless, one can deduce its type (transport) following what happens. Additionally, both objects and activities can be constructed from their parts. In such a setting, type inference cannot only become more complex, but also more helpful, as it allows to collect a complete description of everything in a composed scene, while still being able to detect conflicting or unintended uses.

Техническое описание

Вывод типов — это способность автоматически определять, частично или полностью, тип выражения во время компиляции. Компилятор часто может вывести тип переменной или типовую сигнатуру функции без явных аннотаций типа. Во многих случаях можно полностью опустить аннотации типа из программы, если система вывода типов достаточно надежна, или программа или язык достаточно просты. Для получения информации, необходимой для вывода типа выражения, компилятор либо собирает эту информацию как агрегат и последующее упрощение аннотаций типа, заданных для его подвыражений, либо посредством неявного понимания типа различных атомарных значений (например, `true : Bool`; `42 : Integer`; `3.14159 : Real`; и т. д.). Именно благодаря распознаванию возможного сведения выражений к неявно типизированным атомарным значениям компилятор языка с выводом типов способен полностью компилировать программу без аннотаций типа. В сложных формах программирования высшего порядка и полиморфизма компилятору не всегда удается сделать вывод, и иногда аннотации типа необходимы для устранения неоднозначности. Например, известно, что вывод типов с полиморфной рекурсией является неразрешимой задачей. Кроме того, явные аннотации типа могут быть использованы для оптимизации кода, заставляя компилятор использовать более конкретный (быстрый/компактный) тип, чем он вывел. Некоторые методы вывода типов основаны на решении ограничений или выполнимости по модулю теорий.

Алгоритм вывода типа Хиндли-Милнера

Алгоритм, впервые использованный для вывода типов, теперь неофициально называют алгоритмом Хиндли-Милнера, хотя правильно было бы приписывать его Дамасу и Милнеру. Он также традиционно известен как реконструкция типов. Независимо от работы Хиндли, был предложен эквивалентный алгоритм, Алгоритм W. В 1982 году Луис Дамас. Алгоритмы вывода типов также используются в некоторых системах грамматической индукции и грамматиках, основанных на ограничениях, для естественных языков.