Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Введение
В теории типов, система типов обладает свойством главного типа, если для заданного терма и окружения существует главный тип для этого терма в этом окружении, то есть тип, такой что все остальные типы для этого терма в этом окружении являются экземплярами главного типа. Свойство главного типа является желательным для системы типов, поскольку оно предоставляет способ типизировать выражения в заданном окружении типом, который охватывает все возможные типы выражений, вместо того чтобы иметь несколько несравнимых возможных типов. Вывод типов для систем, обладающих свойством главного типа, обычно стремится вывести главный тип. Например, система ML обладает свойством главного типа, и главные типы выражения могут быть вычислены алгоритмом унификации Робинсона, который используется в алгоритме вывода типов Хиндли-Милнера. Однако многие расширения системы типов ML, такие как полиморфная рекурсия, могут сделать вывод главного типа неразрешимым. Другие расширения, такие как обобщенные алгебраические типы данных в Haskell, разрушают свойство главного типа языка, требуя использования аннотаций типов или заставляя компилятор "угадывать" предполагаемый тип из нескольких вариантов. Свойство главного типирования требует, чтобы для заданного терма существовал типирование (то есть пара, состоящая из контекста и типа), являющееся экземпляром всех возможных типирований этого терма. Свойство главного типирования можно спутать со свойством главного типа, но они различны. Свойство главного типа опирается на контекст как входные данные для определения типа, в то время как свойство главного типирования выдает контекст в качестве результата.
In type theory, a type system is said to have the principal type property if, given a term and an environment, there exists a principal type for this term in this environment, i. e. a type such that all other types for this term in this environment are an instance of the principal type. The principal type property is a desirable one for a type system, as it provides a way to type expressions in a given environment with a type which encompasses all of the expressions' possible types, instead of having several incomparable possible types. Type inference for systems with the principal type property will usually attempt to infer the principal type. For instance, the ML system has the principal type property and principal types for an expression can be computed by Robinson's unification algorithm, which is used by the Hindley–Milner type inference algorithm. However, many extensions to the type system of ML, such as polymorphic recursion, can make the inference of the principal type undecidable. Other extensions, such as Haskell's generalized algebraic data types, destroy the principal type property of the language, requiring the use of type annotations or the compiler to "guess" the intended type from among several options. The principal typing property requires that, given a term, there exist a typing (i. e. a pair with a context and a type) which is an instance of all possible typings of the term. The principal typing property can be confused with the principal type property but is distinct. The principal type property relies on the context as an input to determine the type, but the principal typing property outputs the context as a result.