В теории типов , система типа называется иметь основной тип собственности , если данный термин и окружающую среду, существует основной тип для этого термина в этой среде, то есть такого типа, что все другие типы для этого термина в этой среде являются экземпляром основного типа.
Свойство основного типа является желательным для системы типов, поскольку оно обеспечивает способ набирать выражения в данной среде с типом, который охватывает все возможные типы выражений, вместо того, чтобы иметь несколько несравнимых возможных типов. Вывод типа для систем со свойством основного типа обычно будет пытаться вывести основной тип.
Например, система машинного обучения имеет свойство основного типа, и основные типы для выражения могут быть вычислены с помощью алгоритма унификации Робинсона , который используется алгоритмом вывода типа Хиндли – Милнера . Однако многие расширения системы типов ML, такие как полиморфная рекурсия , могут сделать вывод о главном типе неразрешимым. Другие расширения, такие как Haskell «s обобщенных алгебраические типов данных , уничтожить основной тип свойство языка, что требует использования аннотаций типа или компилятора„угадать“предполагаемый тип из нескольких вариантов.
Свойство основного типа не следует путать с основным свойством типизации, которое требует, чтобы для данного термина существовала типизация (т. Е. Пара с контекстом и типом), которая является экземпляром всех возможных типизаций термина. [1]