Кіріспе

Типтелген лямбда-есептеуі
электрондық транс музыкасының әртісі
System F (сонымен қатар полиморфты лямбда-есептеуі немесе екінші реттік лямбда-есептеуі) – типтер бойынша әмбебап квантификация механизмін жай типтелген лямбда-есептеуіне қосатын типтелген лямбда-есептеуі. System F бағдарламалау тілдеріндегі параметрлік полиморфизмді формалдайды, осылайша Haskell және ML сияқты тілдердің теориялық негізін құрайды. Оны логик Жан-Ив Жирар (1972) және компьютер ғалымы Джон К. Рейнольдс тәуелсіз түрде ашты. Жай типтелген лямбда-есептеуінде терминдер бойынша және оларға байланыстырушылар болса, System F қосымша типтер бойынша және оларға байланыстырушылар бойынша айнымалыларға ие. Мысалы, сәйкестік функциясы A → A түріндегі кез келген типке ие болуы мүмкін деген фактіні System F жүйесінде келесідей сот ретінде формалдауға болады:

мұндағы – типтік айнымалы. Үлкен әріптер дәстүрлі түрде типтік деңгейдегі функцияларды белгілеу үшін қолданылады, ал кіші әріптер – мәндік деңгейдегі функцияларды белгілеу үшін қолданылады. (Көтеріңкі жазылған x, x-тің типін білдіреді; екінқаттан кейінгі өрнек – одан бұрынғы лямбда өрнегінің типі.) Терминді қайта жазу жүйесі ретінде System F қатаң түрде нормалданады. Дегенмен, System F жүйесіндегі типтік қорытынды (нақты типтік түсіндірмелерсіз) шешілмейтін мәселе болып табылады. Керри-Ховард изоморфизмі бойынша System F тек әмбебап квантификацияны қолданатын екінші реттік интуиционистік логиканың фрагментіне сәйкес келеді. System F лямбда кубтың бір бөлігі ретінде қарастырылуы мүмкін, сонымен қатар тәуелді типтері бар, одан да экспрессивті типтелген лямбда-есептеулерімен бірге. Жирардың сөзіне сүйенсек, System F жүйесіндегі "F" әрпі кездейсоқ таңдалған.

Бағдарламалау тілдерінде қолдану

Бұл мақалада қолданылған F жүйесінің нұсқасы, нақты типтелген немесе Шіркеу стиліндегі есептеу болып табылады. λ-терминдеріндегі типтік ақпарат типтік тексеруді оңайлатады. Джо Уэллс (1994) типтік тексерудің System F-тің Карри стиліне сәйкес келетін түрі үшін шешілмейтінін дәлелдеп, "ұятты ашық мәселені" шешті, яғни нақты типтеу белгілемелері жоқ. Уэллстің нәтижесі F жүйесі үшін типтік қорытындының мүмкін еместігін көрсетеді. System F-тің "Hindley–Milner" немесе жай ғана "HM" деп аталатын шектеулі нұсқасы оңай типтік қорытынды алгоритміне ие және Haskell 98 және ML отбасы сияқты көптеген статикалық типтелген функционалдық бағдарламалау тілдерінде қолданылады. Уақыт өте келе, HM стиліндегі типтік жүйелердің шектеулері анықталғанда, тілдер өздерінің типтік жүйелері үшін көбірек экспрессивті логикаға қарай бірте-бірте өтті. GHC – Haskell компиляторы, HM-нан (2008 жылғы жағдай бойынша) асып, синтаксистік емес типтік теңдікпен кеңейтілген System F қолданады; OCaml-дің типтік жүйесіндегі HM емес мүмкіндіктерге GADT кіреді.

Жирард-Рейнольдс изоморфизмі

Екінші реттік интуиционисттік логикада екінші реттік полиморфты лямбда-есептеуі (F2) Жирар (1972) және тәуелсіз түрде Рейнольдс (1974) тарапынан ашылды.

F< жүйесі:

F< жүйесі, "F суб" деп аталады, F жүйесіне қосымша субтиптеу мүмкіндігі қосылған нұсқасы. F<: жүйесі 1980-жылдардан бері бағдарламалау тілдері теориясындағы маңызды мәселе болып табылады, себебі ML отбасы тілдері сияқты функционалдық бағдарламалау тілдерінің негізі параметрлік полиморфизм мен жазбалардың субтиптеуін қолдайды, бұл мүмкіндіктерді F<: жүйесінде бейнелеуге болады.