Основной тип

В теории типов говорят , что система типов имеет свойство основного типа , если для данного терма и среды существует основной тип для этого терма в этой среде, т. е. тип такой, что все другие типы для этого терма в этой среде являются экземплярами основного типа.

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

Например, система ML имеет свойство основного типа, и основные типы для выражения могут быть вычислены с помощью алгоритма унификации Робинсона , который используется алгоритмом вывода типов Хиндли–Милнера . Однако многие расширения системы типов ML, такие как полиморфная рекурсия , могут сделать вывод основного типа неразрешимым. Другие расширения, такие как обобщенные алгебраические типы данных Haskell , разрушают свойство основного типа языка, требуя использования аннотаций типов или компилятора для «угадывания» предполагаемого типа среди нескольких вариантов.

Свойство главного типа требует, чтобы для данного термина существовала типизация (т. е. пара с контекстом и типом), которая является экземпляром всех возможных типизаций термина. Свойство главного типа можно спутать со свойством главного типа, но это нечто иное. Свойство главного типа опирается на контекст как на вход для определения типа, но свойство главного типа выводит контекст как результат. ^[1]

${\displaystyle \Гамма \!\vdash}$

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

• в
• т
• е