Негізгі түрі - Principal type

Жылы тип теориясы, а типтік жүйе бар деп айтылады негізгі түрі меншік, егер термин мен орта берілген болса, бар негізгі түрі осы ортадағы осы термин үшін, яғни осы ортадағы осы термин үшін барлық басқа типтер данасы негізгі типтегі.

Негізгі тип қасиеті типтік жүйе үшін қажет, өйткені ол берілген өрнектегі өрнектерді бірнеше салыстыруға болмайтын бірнеше типтерге ие болудың орнына, өрнектердің барлық мүмкін түрлерін қамтитын типпен теру тәсілін ұсынады. Қорытынды негізгі типтік қасиеті бар жүйелер үшін әдетте негізгі типті шығаруға тырысады.

Мысалы, ML жүйенің негізгі типтік қасиеті бар және өрнектің негізгі типтерін есептеуге болады Робинсонның бірігу алгоритмі арқылы қолданылады Хинди-Милнер түріндегі қорытынды алгоритм. Алайда, ML типтік жүйесіне көптеген кеңейтулер, мысалы полиморфты рекурсия, негізгі типтің қорытындысын шешілмейтін етіп жасай алады. Сияқты басқа кеңейтулер, мысалы Хаскелл Келіңіздер деректердің жалпыланған алгебралық түрлері, пайдалануды талап ететін тілдің негізгі типтік қасиетін жойыңыз аннотацияларды жазыңыз немесе компилятор бірнеше нұсқалардың ішінен жоспарланған түрін «болжауға» мүмкіндік береді.

Негізгі тип сипатын .мен шатастыруға болмайды негізгі теру мерзімді ескере отырып, терминнің барлық мүмкін терулерінің данасы болып табылатын терудің (яғни контекст пен типтің жұбы) болуын талап ететін қасиет.[1]

Әдебиеттер тізімі