Основной тип

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

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

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

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