Типтер теориясындағы негізгі тип қасиеті, термин үшін барлық басқа типтердің жалпылануын қамтамасыз етеді. ML жүйесінде қолданылады, бірақ кеңейтімдермен қиындауы мүмкін.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
Тип теориясында, егер термин мен орта берілгенде, осы ортада осы термин үшін негізгі тип болса, яғни осы ортадағы осы терминнің барлық басқа типтері негізгі типтің инстанциясы болып табылатын болса, онда типтік жүйеде негізгі типтік қасиет бар деп айтылады. Негізгі типтік қасиет типтік жүйе үшін қажетті, себебі ол бірнеше салыстыруға келмейтін мүмкін типтердің болуының орнына, берілген ортада өрнектерді өрнектердің барлық мүмкін типтерін қамтитын типпен типтеуге мүмкіндік береді. Негізгі типтік қасиеттері бар жүйелер үшін типтік қорытындылау әдетте негізгі типті қорытындылауға бағытталған. Мысалы, ML жүйесі негізгі типтік қасиетке ие және өрнектің негізгі типтерін Робинзонның біріктіру алгоритмі арқылы есептеуге болады, ол Хиндли-Милнердің типтік қорытындылау алгоритмінде қолданылады. Дегенмен, ML типтік жүйесінің көптеген кеңейтімдері, мысалы полиморфты рекурсия, негізгі типті қорытындылауды шешілмейтін мәселе етіп жасай алады. Басқа кеңейтімдер, мысалы, Хаскеллдің жалпыланған алгебралық дерек типтері, тілдің негізгі типтік қасиеттерін жояды, сондықтан типтік түсіндірмелерді пайдалануды немесе компилятордың бірнеше нұсқаның ішінде көзделген типті "таңдауын" қажет етеді. Негізгі типтеу қасиеті термин берілген кезде, терминнің барлық мүмкін типтеулерінің инстанциясы болып табылатын типтеудің (яғни контекст пен типтен тұратын жұптың) болуын талап етеді. Негізгі типтеу қасиетін негізгі типтік қасиетпен шатастыруға болады, бірақ олар ерекше. Негізгі типтік қасиет типті анықтау үшін кіріс ретінде контекстке сүйенеді, ал негізгі типтеу қасиеті нәтиже ретінде контекстті шығарады.
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.