Parametrický polymorfismus

Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 12. dubna 2021; kontroly vyžadují 5 úprav .

Parametrický polymorfismus v programovacích jazycích a teorii typů je vlastnost sémantiky typového systému , která umožňuje zpracovávat hodnoty různých typů identickým způsobem, to znamená fyzicky spouštět stejný kód pro data různých typů. [1] [2] .

Parametrický polymorfismus je považován za „opravdovou“ formu polymorfismu [3] , díky čemuž je jazyk výraznější a výrazně zvyšuje opětovné použití kódu . Tradičně se staví proti ad-hoc-polymorfismu [1] , který poskytuje jediné rozhraní pro potenciálně odlišný kód pro různé typy povolené v daném kontextu, potenciálně nekompatibilní ( staticky nebo dynamicky ). V řadě kalkulů, jako je teorie kvalifikovaných typů , je ad-hoc polymorfismus považován za speciální případ parametrického polymorfismu.

Parametrický polymorfismus je základem typových systémů jazyků v rodině ML ; systémy tohoto typu se nazývají polymorfní. V komunitách jazyků s nepolymorfními typovými systémy (potomci Algol a BCPL [4] ) se parametricky polymorfní funkce a typy nazývají „ zobecněné “.

Typový polymorfismus

Termín „ parametrický polymorfismus “ se tradičně používá pro typově bezpečný parametrický polymorfismus, ačkoli existují i jeho netypizované formy (viz parametrický polymorfismus v C a C++ ) [4] . Klíčovým konceptem typově bezpečného parametrického polymorfismu je vedle polymorfní funkce polymorfní typ .

Polymorfní typ ( angl. polymorphic type ) nebo polytype ( angl. polytype ) je typ parametrizovaný jiným typem. Parametr v typové vrstvě se nazývá typová proměnná (nebo typová proměnná) .

Formálně je typový polymorfismus studován v polymorfně typovaném lambda kalkulu , nazývaném Systém F.

Například funkci appendzřetězení dvou seznamů do jednoho lze sestavit bez ohledu na typ prvků seznamu. Nechť proměnná type a popisuje typ prvků seznamu. Potom lze funkci appendzadat jako " forall a. [a] × [a] -> [a]" (zde konstrukce [a]znamená typ " seznam, jehož každý prvek má typa " - syntaxe přijatá v jazyce Haskell ). V tomto případě se říká, že typ je parametrizován proměnnou apro všechny hodnoty a. V každém místě aplikace appendna konkrétní argumenty je hodnota avyřešena a každá její zmínka v podpisu typu je nahrazena hodnotou odpovídající kontextu aplikace. V tomto případě tedy podpis typu funkce vyžaduje, aby typy prvků obou seznamů a výsledek byly totožné .

Sada platných hodnot pro typovou proměnnou je dána kvantifikací . Nejjednodušší kvantifikátory jsou univerzální (jako v příkladu s append) a existenciální (viz níže).

Kvalifikovaný typ je polymorfní typ, navíc vybavený sadou predikátů , které regulují rozsah platných hodnot pro parametr tohoto typu. Jinými slovy, kvalifikace typu vám umožňuje řídit kvantifikaci libovolným způsobem. Teorii kvalifikovaných typů vybudoval Mark P. Jones v roce 1992 [5] . Poskytuje společné zdůvodnění pro nejexotičtější typové systémy, včetně typových tříd , rozšiřitelných zápisůa podtypů , a umožňuje přesné formulování specifických omezení pro konkrétní polymorfní typy, čímž vytváří vztah mezi parametrickými a ad-hoc polymorfismus ( přetěžování ) a mezi explicitním a implicitním přetěžováním. Spojení typu s predikátem v této teorii senazývá důkaz . Algebra podobná lambda kalkulu je formulována pro důkazy , včetně abstrakce důkazů, aplikace důkazů atd. Korelace termínu této algebry s výslovně přetíženou funkcíse nazývá překlad důkazů .

Motivujícími příklady pro vývoj zobecněné teorie byly třídy typu Wadler-Blott a typizace rozšiřitelných záznamů prostřednictvím predikátů Harper-Pearce [5] [6] .

Klasifikace polymorfních systémů

Parametricky polymorfní typové systémy jsou zásadně klasifikovány podle hodnosti a predikativní vlastnosti . Kromě toho se rozlišuje explicitní a implicitní polymorfismus [7] a řada dalších vlastností. Implicitní polymorfismus je poskytován prostřednictvím odvození typu , což výrazně zlepšuje použitelnost, ale má omezenou expresivitu. Mnoho praktických parametricky polymorfních jazyků odděluje fáze externího implicitně typovaného jazyka a interního explicitně typovaného jazyka .

Nejobecnější formou polymorfismu je „ nepredikativní polymorfismus vyšší úrovně “. Nejoblíbenějšími omezeními této formy jsou polymorfismus 1. úrovně nazývaný " prenex " a predikativní polymorfismus . Společně tvoří " predikativní prenexový polymorfismus " podobný tomu implementovanému v ML a dřívějších verzích Haskellu .

Jak se typové systémy stávají složitějšími, stávají se typové signatury tak složité, že jejich úplné nebo téměř úplné odvození je mnohými výzkumníky považováno za kritickou vlastnost, jejíž absence způsobí, že jazyk nebude vhodný pro praxi [8] [9] . Například u tradičního kombinátoru má mapúplný typový podpis (s přihlédnutím ke generické kvantifikaci) v rámci typově bezpečného sledování toku výjimek následující formu [10] [8] (jak je uvedeno výše , znamená seznam prvky typu ):[a]a
$val\;map\colon \forall \alpha \colon \star _{\cdot }\forall \beta \colon \star _{\cdot }\forall \gamma \colon \emptyset _{\cdot }\forall \delta \colon \emptyset _{\cdot }(\;\alpha {\xšipka doprava {\gamma }}\beta \;)\;{\xšipka doprava {\delta }}\;(\;\left[\alpha \ vpravo]{\xšipka vpravo {\gamma }}\levá[\beta \vpravo]\;)$

Pořadí

Pořadí polymorfismu ukazujehloubku vnoření kvantifikátorů typových proměnných povolených v rámci systému . " Polymorfismus hodnosti k " (pro k > 1 ) umožňuje specifikovat typové proměnné podle polymorfních typů hodnosti ne vyšší než ( k - 1) . " Polymorfismus vyšších řádů " umožňuje umístit kvantifikátory typových proměnných nalevo od libovolného počtu šipek v typech vyšších řádů .

Joe Wells dokázal [ 11] , že odvození typu pro systém F typu Curry není rozhodnutelné pro hodnosti nad 2, takže při použití vyšších hodností musí být použita explicitní anotace typu [12] .

Existují systémy částečného inferenčního typu , které vyžadují, aby byly anotovány pouze proměnné typu , které nelze odvodit [13] [14] [15] .

Polymorfismus Prenex

Polymorfismus úrovně 1 se často nazývá prenexový polymorfismus (od slova "prenex" - viz prenex normální forma ). V prenexovém polymorfním systému nelze typové proměnné konkretizovat pomocí polymorfních typů. Toto omezení činí rozlišení mezi monomorfními a polymorfními typy zásadním, a proto se v systému prenex polymorfní typy často nazývají „ typovací schémata “ ( anglicky typová schémata ), aby se odlišily od „obyčejných“ (monomorfních) typů (monotypů). V důsledku toho mohou být všechny typy zapsány ve formě, když jsou všechny kvantifikátory typových proměnných umístěny na nejvzdálenější (prenex) pozici, která se nazývá prenexová normální forma . Jednoduše řečeno, definice polymorfních funkcí jsou povoleny, ale polymorfní funkce nelze předávat jako argumenty jiným funkcím [16] [17] - polymorfně definované funkce musí být před použitím monotypově konkretizovány.

Blízkým ekvivalentem je takzvaný „ Let-polymorfismus “ nebo „ polymorfismus ve stylu ML “ od Damas-Milnera. Technicky má Let-polymorfismus v ML další syntaktická omezení, jako je „ omezení hodnoty “ spojené s problémy s bezpečností typu při použití odkazů (které se nevyskytují v čistých jazycích, jako je Haskell a Clean ) [18] [19] .

Predikativita

Predikativní polymorfismus

Predikativní (podmíněný) polymorfismus vyžaduje, aby typová proměnná byla konkretizována monotypem (nikoli polytypem).

Predikativní systémy zahrnují intuicionistickou teorii typů a Nuprl .

Nepredikativní polymorfismus

Impredikativní (nepodmíněný) polymorfismus umožňuje vytvořit instanci typové proměnné s libovolným typem – jak monomorfním, tak polymorfním, včetně typu, který je definován. (Umožnění, aby systém v rámci kalkulu rekurzivně zahrnoval sám sebe do sebe, se nazývá impredikativita . Potenciálně to může vést k paradoxům jako Russell nebo Cantor [20] , ale to se nestane v případě propracovaného typového systému [21] .)

Nepredikativní polymorfismus umožňuje předávat polymorfní funkce jiným funkcím jako parametry, vracet je jako výsledek, ukládat je do datových struktur atd., proto se také nazývá prvotřídní polymorfismus . Toto je nejvýkonnější forma polymorfismu, ale na druhé straně představuje vážný problém pro optimalizaci a činí odvození typu neřešitelným .

Příkladem impredikativního systému je Systém F a jeho rozšíření (viz lambda kostka ) [22] .

Podpora rekurze

Tradičně v potomcích ML může být funkce polymorfní pouze při pohledu „zvenčí“ (to znamená, že ji lze aplikovat na argumenty různých typů), ale její definice může obsahovat pouze monomorfní rekurzi (tj. rozlišení typu je provedené před hovorem). Rozšíření rekonstrukce typu ML na rekurzivní typy nepředstavuje žádné vážné potíže. Na druhou stranu kombinace rekonstrukce typu s rekurzivně definovanými pojmy vytváří obtížný problém známý jako polymorfní rekurze . Mycroft a Meertens navrhli polymorfní typovací pravidlo, které umožňuje instanci rekurzivních volání rekurzivní funkce z jejího vlastního těla s různými typy. V tomto kalkulu, známém jako Milner-Mycroftův kalkul, je odvození typu nerozhodnutelné . [23]

Polymorfismus strukturního typu

Typy produktů (také známé jako „ záznamy “) slouží jako formální základ pro objektově orientované a modulární programování. Jejich duální pár se skládá ze součtových typů (také známých jako " varianty ") [24] [25] [19] :

\neg \lbrace a\land b\rbrace =\langle \neg a\lor \neg b\rangle

\neg \langle a\lor b\rangle =\lbrace \neg a\land \neg b\rbrace

Společně jsou prostředkem k vyjádření jakýchkoli složitých datových struktur a některých aspektů chování programů .

Record calculi je zobecněný název pro problém a řadu jeho řešení týkajících se flexibility typů produktů v programovacích jazycích pod podmínkou typové bezpečnosti [26] [27] [28] . Tento termín se často rozšiřuje na typy součtů a hranice pojmu " typ záznamu " se mohou lišit počet od počtu (stejně jako samotný pojem " typ ". Používají se také termíny „ polymorfismus záznamu “ (který opět často zahrnuje variantní polymorfismus ) [27] , „ modulový počet “ [9] a „ strukturní polymorfismus “.

Obecné informace

Typové součiny a součty ( záznamy a varianty [ en ] poskytují flexibilitu při vytváření složitých datových struktur, ale omezení mnoha systémů reálného typu často brání jejich použití ve skutečné flexibilitě. Tato omezení obvykle vznikají kvůli problémům s efektivitou, odvozením typu nebo jednoduše použitelností. [29]

Klasickým příkladem je Standard ML , jehož typový systém byl záměrně omezen tak, aby se snoubila snadnost implementace s výrazností a matematicky prokazatelnou typovou bezpečností .

Příklad definice záznamu :

> val r = { name = "Foo" , used = true }; (* val r : {name : string, used : bool} = {name = "Foo", used = true} *)

Přístup k hodnotě pole podle jeho názvu se provádí pomocí prefixové konstrukce formuláře #field record:

> val r1 = #jméno r ; (* val r1 : string = "Foo" *)

Následující definice funkce nad záznamem je správná:

> fun name1 ( x : { name : string , age : int }) = # name x

A následující generuje chybu kompilátoru, že typ není plně vyřešen :

> fun name2 x = #name x (* nevyřešený typ v deklaraci: {name : '1, ...} *)

Monomorfismus záznamů je činí neflexibilními, ale účinnými [30] : protože skutečné umístění v paměti každého pole záznamu je známo předem (v době kompilace), odkazování na něj jménem se zkompiluje do přímého indexování, které se obvykle vypočítává na jednom počítači. návod. Při vývoji složitých škálovatelných systémů je však žádoucí mít možnost abstrahovat pole z konkrétních záznamů – například definovat univerzální selektor polí:

zábava vyberte r l = #l r

Kompilace polymorfního přístupu k polím, která mohou být v různých záznamech v různém pořadí, je ale obtížný problém, a to jak z pohledu bezpečnostní kontroly operací na jazykové úrovni, tak z pohledu výkonu na úrovni strojového kódu. Naivním řešením může být dynamické vyhledávání slovníku při každém volání (a skriptovací jazyky jej používají), ale to je zjevně extrémně neefektivní. [31]

Typové součty tvoří základ větveného výrazu a vzhledem k přísnosti typového systému poskytuje kompilátor kontrolu nad úplností analýzy. Například pro následující typ součtu :

datový typ 'a foo = A z 'a | B z ( 'a * 'a ) | C

jakákoli funkce nad tím bude vypadat

zábavný bar ( p : 'a foo ) = případ p z A x => ... | B ( x , y ) => ... | c => ...

a když jsou některé klauzule odstraněny, kompilátor vydá varování o neúplné analýze (" match nonexhaustive"). Pro případy, kdy pouze několik z mnoha možností vyžaduje analýzu v daném kontextu, je možné uspořádat defaultvětvení pomocí tzv. "Joker" - univerzální vzorek, se kterým jsou všechny platné (podle psaní) hodnoty srovnatelné. Píše se s podtržítkem (" _"). Například:

zábavný bar ( p : 'a foo ) = případ p z C => ... | _ => ...

V některých jazycích (ve Standard ML , v Haskell ) je i „jednodušší“ konstrukce if-then-elsejen syntaktický cukr nad speciálním případem větvení , tedy výraz

když A , tak B jinak C

již ve fázi gramatické analýzy je prezentován ve formě

případ A pravdy = > B | nepravda => C

nebo

případ A pravdy = > B | _ => C

Syntaktický cukr

Ve standardním ML jsou záznamy a varianty monomorfní, nicméně je podporován syntaktický cukr pro práci se záznamy s více poli, nazývaný " univerzální vzor " [32] :

> val r = { name = "Foo" , used = true }; (* val r : {jméno : řetězec, použité : bool} = {jméno = "Foo", použité = pravda} *) > val { použité = u , ...} = r ; (* val u : bool = true *)

Tři tečky v typu „ {used, ...}“ znamenají, že v tomto záznamu existují kromě zmíněných i další pole. Neexistuje však žádný polymorfismus záznamu jako takový (ani prenex ): je vyžadováno plné statické rozlišení informace o typu monomorfního záznamu (přes odvození nebo explicitní anotaci ).

Rozšíření a funkční aktualizace záznamů

Pojem rozšiřitelné záznamy se používá pro zobecněné označení takových operací jako expanze (vytvoření nového záznamu na základě existujícího s přidáním nových polí), řezání (převzetí určené části z existujícího záznamu) atd. z toho vyplývá možnost tzv. „ aktualizace funkčního záznamu “ ( aktualizace funkčního záznamu ) - operace sestrojení nové hodnoty záznamu na základě stávajícího zkopírováním názvů a typů jeho polí, ve kterých je jedno nebo více polí v nový záznam obdrží nové hodnoty, které se liší od původních (a případně mají jiný typ). [33] [34] [19] [35] [36] [37]

Operace funkční aktualizace a rozšíření jsou samy o sobě ortogonální pro záznam polymorfismu, ale jejich polymorfní použití je zvláště zajímavé. Dokonce i u monomorfních záznamů je důležité mít možnost vynechat explicitní zmínku o polích, která jsou zkopírována beze změny, což ve skutečnosti představuje polymorfismus záznamu v čistě syntaktické formě . Na druhou stranu, pokud považujeme všechny záznamy v systému za rozšiřitelné, pak to umožňuje, aby funkce na záznamech byly typovány jako polymorfní.

Příklad nejjednodušší varianty návrhu je implementován v Alice ML (podle současných nástupnických konvencí ML ) [36] . Univerzální vzor (elipsa ) má rozšířené možnosti: lze jej použít k „zachycení řádku“, aby bylo možné pracovat se „zbývající“ částí záznamu jako hodnotou:

> val r = { a = 1 , b = pravda , c = "ahoj" } (* r = {a = 1, b = pravda, c = "ahoj"} *) > val { a = n , ... = r1 } = r (* r1 = {b=pravda, c="ahoj"} *) > hodnota r2 = { d = 3,14 , ... = r1 } (* r2 = {b=pravda, c="ahoj ", d=3,14} *)

Funkční aktualizace je implementována jako derivát zachycení řádku se servisním slovem where. Například následující kód:

> nechť hodnota r = { a = 1 , c = 3,0 , d = "není seznam" , f = [ 1 ], p = [ "není řetězec" ], z = NONE } v { r , kde d = nula , p = "ahoj" } konec

se automaticky přepíše do tvaru:

> nechť val r = { a = 1 , c = 3,0 , d = "není seznam" , f = [ 1 ], p = [ "není řetězec" ], z = ŽÁDNÝ } val { d = _, p = _, ... = tmp } = r v { ... = tmp , d = nula , p = "ahoj" } konec

Zřetězení záznamu

Jeden z prvních (konec 80. let - začátek 90. let 20. století ) navrhoval různé možnosti pro formalizaci rozšiřitelných záznamů pomocí operací zřetězení na nepolymorfních záznamech (Harper-Pearce [38] , Wand [39] , Salzmann [40] ). Cardelli dokonce v jazyce Amber používal místo polymorfismu záznamové operace . Neexistuje žádný známý způsob, jak tyto výpočty efektivně sestavit; tyto výpočty jsou navíc velmi složité z hlediska typově teoretické analýzy. [27] [41] [42] [43]

Například [33] :

val car = { name = "Toyota" ; věk = "starý" ; id = 6678 } val truck = { name = "Toyota" ; id = 19823235 } ... val repaired_truck = { osobní a nákladní automobil }

polymorfismu řádků ) ukázal, že vícenásobnou dědičnost lze modelovat pomocí zřetězení záznamů [39] [33] .

Strukturální podtypování od Cardelliho

Luca Cardelli prozkoumal možnostformalizace „ polymorfismu záznamu “ prostřednictvím vztahů podtypů na záznamech: k tomu je záznam považován za „univerzální podtyp“, to znamená, že jeho hodnota může odkazovat na celý soubor jeho supertypů. Tento přístup také podporuje dědičnost metod a slouží jako typově teoretický základ pro nejběžnější formy objektově orientovaného programování . [27] [44] [45]

Cardelli představil variaci na metodu kompilace polymorfismu záznamu napříč jejich podtypy předdefinováním offsetu všech možných štítků v potenciálně obrovské struktuře s mnoha prázdnými sloty [31] .

Metoda má značné nevýhody. Podpora podtypování v typovém systému značně komplikuje mechanismus kontroly typové konzistence [46] . Navíc v jeho přítomnosti přestává statický typ výrazu poskytovat úplnou informaci o dynamické struktuře hodnoty položky . Pokud například používáte pouze podtypy, následující výraz:

> pokud je pravda , pak { A = 1 , B = pravda } else { B = nepravda , C = "Kočka" } (* val it : {B : bool} *)

má typ {B : bool}, ale jeho dynamická hodnota je rovna {A = 1, B = true}, to znamená, že se informace o typu rozšířeného záznamu ztratí [43] , což je vážný problém pro kontrolu operací, které pro své provedení vyžadují kompletní informace o struktuře hodnot (jako např. srovnání pro rovnost ) [19] . Konečně, v přítomnosti podtypů výběr mezi uspořádanou a neuspořádanou reprezentací záznamů vážně ovlivňuje výkon [47] .

Popularita podtypování je způsobena tím, že poskytuje jednoduchá a vizuální řešení mnoha problémů. Například objekty různých typů mohou být umístěny do jednoho seznamu, pokud mají společný nadtyp [48] .

Wanda řádkový polymorfismus

Mitchell Wand v roce 1987 navrhl myšlenku(ne výslovně specifikované) části záznamu prostřednictvím toho, co nazval proměnná typu řádku ( proměnná typu řádku ) [49] .

Řádková proměnná je proměnná typu , která prochází množinou konečných sad (řádků) typovaných polí (párů " (значение : тип)"). Výsledkem je schopnost implementovat širokou škálu dědičnosti přímo nad parametrickým polymorfismem, který je základem ML , aniž by se typový systém komplikoval pravidly pro podtypování Výsledný druh polymorfismu se nazývá řádkový polymorfismus . Inline polymorfismus se vztahuje jak na součiny typů , tak na součty typů .

Vand si tento termín vypůjčil z angličtiny. řádek (řádek, řetěz, čára) z Algol-68 , kde to znamenalo soubor pohledů. V ruskojazyčné literatuře se tento termín v kontextu Algolu tradičně překládá jako „vícedruhové“. Existuje také překlad „řádkových proměnných“ jako „řetězcové proměnné“ [41] , což může způsobit zmatek s malými písmeny v typech řetězců .

Příklad ( jazyk OCaml ; syntaxe postfixu, record#field) [50] :

# let send_m a = a # m ;; (* hodnota send_m : < m : a; .. > -> a = <zábava> *)

Tři tečky (dvou teček) jsou akceptovanou syntaxí OCaml pro nepojmenovanou proměnnou typu inline . Díky tomuto typování lze funkci send_maplikovat na objekt libovolného (dříve neznámého ) typu objektu, který zahrnuje metodu modpovídajícího podpisu.

Odpočet typu pro Wanda kalkul v původní verzi byl neúplný: kvůli chybějícím omezením pro rozšíření série nahradí přidání pole, pokud se název shoduje, stávající - v důsledku toho ne všechny programy mají hlavní typ [6] [43] . Tento systém však byl prvním konkrétním návrhem na rozšíření ML o záznamy, které podporují dědičnost [51] . V následujících letech byla navržena řada různých vylepšení, včetně těch, díky nimž je kompletní [51] [27] .

Nejpozoruhodnější stopu zanechal Didier Remy ( francouzsky Didier Rémy ). Vybudoval praktický typový systém s rozšiřitelnými záznamy, včetně kompletního a efektivního algoritmu rekonstrukce typu [52] [53] . Remy stratifikuje jazyk typů na druhy a formuluje seřazenou algebru typů ( angl. sorted algebra of types, sorted language of types ). Rozlišuje se mezi vlastním druhem typů (včetně typů polí) a druhem polí ; jsou zavedena mapování mezi nimi a na jejich základě jsou formulována pravidla pro typování rozšířených záznamů jako jednoduché rozšíření klasických pravidel ML . Informace o přítomnosti pole jsou definovány jako mapování z řazení typu na řazení podle pole . Proměnné typu řádku jsou přeformulovány jako proměnné náležející k řazení pole a rovnající se konstantě absence , což je prvek řazení pole , který nemá shodu v řazení typu . Operace vyhodnocení typu pro záznam n polí je definována jako mapování n-árního pole na typ (kde každé pole v n-tice je buď vypočítáno funkcí přítomnosti nebo dáno konstantou absence ).

Zjednodušeně lze myšlenku kalkulu interpretovat jako rozšíření typu libovolného pole záznamu o příznak přítomnosti/nepřítomnosti a reprezentaci záznamu jako n-tice se slotem pro každé možné pole [6] . V implementačním prototypu byla syntaxe typového jazyka přiblížena typově teoretické formulaci, například [52] :

# let car = { name = "Toyota" ; věk = "starý" ; id = 7866 } ;; (* auto : ∏ (jméno : pre (řetězec); id : pre (číslo); věk : před (řetězec); abs) *) # let truck = { name = "Blazer" ; id = 6587867567 } ;; (* truck : ∏ (name : pre (string); id : pre (num); abs) *) # let person = { name = "Tim" ; věk = 31 ; id = 5656787 } ;; (* osoba : ∏ (jméno : pre (řetězec); id : pre (num); věk : pre (num); abs) *)

(symbol ∏v Remy znamená operaci výpočtu typu)

Přidání nového pole se zapisuje pomocí konstrukce with:

# nechat řidiče = { osoba s vozidlem = auto } ;; (* řidič : ∏ (vozidlo : pre (∏ (jméno : pre (řetězec); id : pre (číslo); věk : pre (řetězec); abs)); jméno : pre (řetězec); id : pre (číslo) ; věk : pre (num); abs) *)

Funkční aktualizace je napsána identicky, s tím rozdílem, že zmínka o již existujícím poli ji přepíše:

# let truck_driver = { řidič s vozidlem = truck };; (* řidič kamionu : ∏ (vozidlo : pre (∏ (jméno : pre (řetězec); id : pre (num); abs)); jméno : pre (řetězec); id : pre (num); věk : pre (číslo ); břišní svaly) *)

Toto schéma formalizuje omezení potřebná pro kontrolu operací na záznamech a odvození hlavního typu, ale nevede ke zřejmé a efektivní implementaci [6] [43] . Remy používá hashování, které je v průměru poměrně efektivní, ale zvyšuje provozní režii i u nativně monomorfních programů a není vhodné pro záznamy s mnoha poli [31] .

Rémy pokračoval ve zkoumání použití inline polymorfismu ve spojení s datovým podtypováním , přičemž zdůraznil, že se jedná o ortogonální koncepty, a ukázal, že záznamy se stávají nejvýraznějšími, když se používají společně [54] . Na tomto základě spolu s Jérômem Vouillonem navrhl odlehčené objektově orientované rozšíření ML [55] . Toto rozšíření bylo implementováno v jazyce Xaviera Leroye "Caml Special Light" a přeměnilo jej na OCaml [56] . Objektový model OCaml je úzce provázán s využitím strukturálního podtypování a inline polymorfismu [48] , proto jsou někdy mylně identifikovány. Inline produktový polymorfismus v OCaml je jádrem odvození typu ; vztahy podtypů nejsou v podporovaném jazyce nutné, ale dále zvyšují flexibilitu v praxi [55] [50] [48] . OCaml má jednodušší a popisnější syntaxi pro informace o typu.

Jacques Garrigue ( fr. Jacques Garrigue ) zavedl [25] praktický systém polymorfních součtů . Zkombinoval teoretickou práci Remiho a Ohoriho , vybudoval systém, který běží uprostřed: informace o přítomnosti značek v záznamu jsou reprezentovány pomocí pohlaví a informace o jejich typech využívají inline proměnné. Aby kompilátor rozlišil mezi polymorfními a monomorfními součty, používá Garriga speciální syntaxi (backtick, prefix tag). To eliminuje potřebu deklarace typu – můžete na něj okamžitě zapisovat funkce a kompilátor vypíše minimální seznam značek, jakmile se tyto funkce skládají. Tento systém se stal součástí OCaml kolem roku 2000 , ale ne místo , ale navíc k monomorfním součtům , protože jsou poněkud méně efektivní a kvůli neschopnosti kontrolovat úplnost analýzy je obtížné najít chyby (na rozdíl od Bloomova řešení ). [25] [57]

Nevýhodou Wandova inline polymorfismu je nesrozumitelnost implementace (neexistuje jediný systematický způsob, jak jej sestavit, každý specifický typový systém založený na inline proměnných má svou vlastní implementaci) a nejednoznačný vztah s teorií (neexistuje jednotná formulace pro typovou kontrolu a inferenci , podpora inference byla řešena samostatně a vyžadovala experimenty s ukládáním různých omezení) [27] .

Průsvitné součty Harper-Lilybridge

Nejsložitějším typem záznamů jsou závislé záznamy. Takové záznamy mohou zahrnovat typy i "běžné" hodnoty (materializované typy, reifikované [9] ) a termíny a typy v dalším pořadí v těle záznamu lze určit na základě těch, které jim předcházejí. . Takové zápisy odpovídají „ slabým součtům “ teorie závislých typů , známé také jako „ existenciály “, a slouží jako nejobecnější zdůvodnění systémů modulů v programovacích jazycích [58] [59] . Cardelli považoval [60] typů podobných vlastnostmi za jeden z hlavních typů v plnotypovém programování (ale nazval je „ n-tice “).

Robert Harper a Mark Lillibridge zkonstruovali [61 ] [59] průsvitný součtový kalkul ,abyformálně ospravedlnili prvotřídní modulový jazyk vyššího řádu , nejpokročilejší známý systém modulů . Tento kalkul se mimo jiné používá v sémantice Harper-Stone , která představuje typově teoretické zdůvodnění Standard ML .

Průhledné součty zobecňují slabé součty prostřednictvím štítků a sady rovností, které popisují konstruktory typů . Pojem průsvitný znamená , že typ záznamu může obsahovat jak typy s explicitně exportovanou strukturou, tak i zcela abstraktní . Vrstva rodů v kalkulu má jednoduché klasické složení: rozlišuje se rod všech typů a funkční rody druhu , typizační typové konstruktory ( ML nepodporuje polymorfismus u vyšších rodů , všechny typové proměnné patří do rodu , a abstrakce typových konstruktorů je možná pouze prostřednictvím funktorů [62 ] ). Kalkulus rozlišuje pravidla pro podtypování pro záznamy jako základní typy a pro pole záznamů jako jejich složky, v tomto pořadí, s ohledem na „podtypy“ a „podpole“, zatímco zakrývání (abstrakce) podpisů polí je samostatný koncept od podtypování. Podtypování zde formalizuje mapování modulů na rozhraní . [61] [9] $\star$ $k_{1}=>k_{2}$ $\star$

Harper-Lilybridgeův kalkul je nerozhodnutelný i z hlediska kontroly typové konzistence ( dialekty modulového jazyka implementované ve Standard ML a OCaml používají omezené podmnožiny tohoto kalkulu). Později však Andreas Rossberg na základě jejich nápadů vybudoval jazyk „ 1ML “, ve kterém jsou tradiční záznamy na úrovni jádra jazyka a struktur na úrovni modulů stejnou prvotřídní konstrukcí [9] (výrazně výraznější než Cardelliho - viz kritika jazyka modulu ML ). Začleněním myšlenky Harpera a Mitchella [63] o rozdělení všech typů do vesmírů „malých“ a „velkých“ typů (zjednodušeně je to podobné základnímu rozdělení typů na jednoduché a agregované typy, přičemž nestejná pravidla pro psaní), Rossberg poskytoval rozlišovací schopnost nejen kontroly konzistence , ale téměř kompletní odvození typu . Navíc 1ML umožňuje nepředvídatelný polymorfismus [64] . Zároveň je vnitřní jazyk v 1ML založen na plochém Systému F ω a nevyžaduje použití závislých typů jako metateorie. Od roku 2015 nechal Rossberg otevřenou možnost přidat inline polymorfismus do 1ML , pouze poznamenal, že by to mělo poskytnout úplnější typové odvození [9] . O rok později přidal [65] efektový polymorfismus k 1ML .

Polymorfní počet záznamů Ohori

Atsushi Ohori spolu se svým nadřízeným Peterem Bunemanem v roce 1988 navrhl myšlenku omezení rozsahu možných hodnot proměnných běžného typu při polymorfním typování samotných záznamů . Později Ohori tuto myšlenku formalizoval prostřednictvím rodů notace , když v roce 1995 vybudoval plnohodnotný počet a metodu pro jeho efektivní kompilaci [19] [30] . Implementační prototyp vznikl v roce 1992 jako rozšíření kompilátoru SML/NJ [66] , poté Ohori vedl vývoj vlastního kompilátoru SML# , který implementuje stejnojmenný dialekt Standard ML . V SML# slouží polymorfismus záznamů jako základ pro bezproblémové vkládání konstrukcí SQL do programů SML . SML# používají velké japonské společnosti k řešení obchodních problémů spojených s vysoce zatíženými databázemi [67] . Příklad takové relace ( REPL ) [68] :

zábavný bohatý { Plat = s , ... } = s > 100000 ; (* val richy = fn : 'a#{ Salary:int, ... } -> bool *) zábava mladí x = #Věk x < 24 ; (* val young = fn : 'a#{ Age:int, ... } -> bool *) legrace youngAndWealthy x = bohatý x a také mladý x ; (* val youngAndWealthy = fn : 'a#{ Age:int, Plat:int, ... } -> bool *) zábava vybrat display l pred = fold ( fn ( x , y ) => if pred x then ( display x ) ::y else y ) l nil ; (* val select = fn : ('a -> 'b) -> 'a seznam -> ('a -> bool) -> 'b seznam *) zábava youngAndWealthyEmployees l = vybrat # Jméno l youngAndWealthy ; (* val youngAndWealthyEmployees = fn : 'b#{ Age:int, Name:'a, Salary:int, ... } list -> 'a list *)

Ohori nazval svůj kalkul „ záznamovým polymorfismem “ ( anglicky record polymorphism ) nebo „ polymorphic record calculus “ ( anglicky polymorphic record calculus ), přičemž zároveň zdůraznil, že stejně jako Wand uvažuje o polymorfismu nejen typů produktů , ale také typů- součty [27] .

Ohori kalkul se vyznačuje nejintenzivnějším využitím rodové vrstvy [6] . V hesle (odkaz typu na rod ) symbol znamená buď rod všech typů ; nebo rod záznamu , který má tvar , označující množinu všech záznamů obsahujících alespoň specifikovaná pole; nebo variantní rod mající tvar označující množinu všech variantních typů obsahujících alespoň specifikované konstruktory . V ploché syntaxi jazyka je omezení typu na nějaký druh zápisu zapsáno jako (viz příklady výše). Řešení je poněkud podobné omezené kvantifikaci Cardelli-Wegnera [27] . $t\colon \colon k$ $t$ $k$ $k$ $U$ ${\displaystyle \left\{\left\{l_{1}\dvojtečka t_{1},\tečky ,l_{n}\dvojtečka t_{n}\vpravo\}\vpravo\))$ $\left\langle \left\langle l_{1}:t_{1},\tečky ,l_{n}\dvojtečka t_{n}\right\rangle \right\rangle$ t#{...}

Jedinou polymorfní operací poskytovanou tímto kalkulem je operace extrakce pole [69] . Ohori však jako první zavedl jednoduché a efektivní schéma kompilace pro polymorfismus záznamů [43] . Nazval to „kalkulus realizací“ ( implementační kalkul ). Záznam je reprezentován vektorem uspořádaným lexikograficky podle názvů polí původního záznamu; adresování pole jménem se převede na volání zprostředkující funkce, která vrátí číslo daného pole v daném vektoru požadovaným názvem, a následné indexování vektoru podle vypočítaného čísla pozice. Funkce je volána pouze při vytváření instancí polymorfních termínů, což při použití polymorfismu představuje minimální režii na běhové prostředí a při práci s monomorfními typy nezatěžuje žádnou režii. Metoda funguje stejně dobře s libovolně velkými položkami a variantami. Kalkulus poskytuje typovou inferenci a nachází silnou shodu s teorií ( obecná kvantifikace přímo souvisí s obvyklým vektorovým indexováním ), je přímým rozšířením Girard-Reynoldsova lambda kalkulu druhého řádu , který umožňuje různé dobře známé vlastnosti polymorfních typizace, která má být převedena na polymorfismus záznamu [31] .

V praxi nebyla podpora pro polymorfní varianty v SML# implementována kvůli její nekompatibilitě s mechanismem definice typu součtu Standard ML (vyžaduje syntaktické oddělení součtů a rekurzivních typů) [70] .

Nevýhodou ohorského kalkulu je chybějící podpora operací expanze nebo zkrácení záznamu [27] [71] [43] .

Prvotřídní značky Guster-Jones

V teorii kvalifikovaných typů jsou rozšiřitelné záznamy popsány absencí pole ( "chybí" predikát ) a přítomností predikátu pole ( "má" predikát ). Benedict Gaster ( Benedict R. Gaster ) ji spolu s autorem teorie Markem Jonesem ( Mark P. Jones ) dopracovali z hlediska rozšiřitelných záznamů k praktickému typovému systému implicitně typovaných jazyků včetně definování způsobu kompilace [6] . Razí termín prvotřídní štítky , aby zdůraznili schopnost abstrahovat operace pole od staticky známých štítků. Později Gaster obhájil svou disertační práci [72] o sestrojeném systému .

Gaster-Jonesův kalkul neposkytuje úplné odvození typu . Navíc bylo kvůli problémům s rozhodností zavedeno umělé omezení: zákaz prázdných sérií [73] . Sulzmann se pokusil přeformulovat kalkul [40] , ale systém, který vytvořil, nelze rozšířit tak, aby podporoval expanzi polymorfních záznamů, a nemá univerzální účinnou metodu kompilace [43] .

Daan Leijen přidal do Gaster-Jonesova kalkulu predikát rovnosti řádků (nebo predikát rovnosti řádků ) a přesunul jazyk řad do jazyka predikátů – to zajistilo úplné odvození typu a zrušilo zákaz prázdných řad [74] . Při kompilaci jsou záznamy převedeny do lexikograficky uspořádané n-tice a překlad důkazů je aplikován podle Gaster-Jonesova schématu. Layenův systém umožňuje vyjádření idiomů , jako jsou zprávy vyššího řádu (nejvýkonnější forma objektově orientovaného programování ) a prvotřídní větve .

Na základě těchto prací byla implementována rozšíření do jazyka Haskell [75] .

Výsledky Gaster-Jones se velmi blíží výsledkům z Ohori , a to i přes značné rozdíly v typově teoretickém zdůvodnění a hlavní výhodou je podpora operací expanze a zkrácení záznamu [6] . Nevýhodou kalkulu je, že se spoléhá na vlastnosti typového systému , které se nenacházejí ve většině programovacích jazyků. Odvozování typu pro něj je navíc vážný problém, a proto autoři zavedli další omezení. A ačkoli Layen odstranil mnoho nedostatků, použití -větve není možné. [71]default

Polymorfismus kontrolní konstrukce

S rozvojem softwarových systémů se může počet možností v typu součtu zvýšit a přidání každé možnosti vyžaduje přidání odpovídající větve ke každé funkci nad tímto typem, i když jsou tyto větve v různých funkcích totožné. Složitost zvyšování funkčnosti ve většině programovacích jazyků tedy závisí nelineárně na deklarativních změnách v zadání. Tento vzor je známý jako problém s výrazem . Dalším dobře známým problémem je zpracování výjimek : v průběhu desetiletí výzkumu typových systémů mohly všechny jazyky klasifikované jako typově bezpečné ukončit vyvoláním nezachycené výjimky – protože navzdory psaní samotných výjimek mechanismus pro vyvolání a manipulace s nimi nebyla napsána. Zatímco nástroje pro analýzu toku výjimek byly vytvořeny, tyto nástroje byly vždy externí vůči jazyku.

Matthias Blume , kolega Andrewa Appela pracující na nástupci projektu ML [76] ), jeho postgraduální student Wonseok Chae a kolega Umut Acar vyřešili oba problémy založené na matematických dualitních součinech a součtech . Ztělesněním jejich myšlenek byl jazyk MLPolyR [71] [34] [77] , založený na nejjednodušší podmnožině Standardu ML a doplněný o několik úrovní typové bezpečnosti [78] . Wonseok Chai později obhájil svou disertační práci o těchto úspěších [78] .

Řešení je následující. Podle principu duality odpovídá úvodní forma pro pojem eliminační formě jeho duálu [ 71] . Vylučovací forma součtů (rozbor větví) tedy odpovídá úvodní formě zápisů. To podporuje větvení, aby mělo stejné vlastnosti, které jsou již dostupné pro záznamy – udělejte z nich prvotřídní objekty a dovolte je rozšiřovat.

Například nejjednodušší interpret jazyka výrazů:

fun eval e = případ e of `Konst i => i | `Plus (e1,e2) => eval e1 + eval e2

se zavedením prvotřídní konstrukce caseslze přepsat jako:

fun eval e = shodu e s případy `Const i => i | `Plus (e1,e2) => eval e1 + eval e2

po kterém caseslze -blok vykreslit:

zábava eval_c eval = případy `Const i => i | `Plus (e1,e2) => eval e1 + eval e2 zábava eval e = shodu e s (eval_c eval)

Toto řešení umožňuje default-větvení (na rozdíl od Gaster-Jonesova kalkulu ), které je důležité pro skladbu prvotřídních poboček [34] . Dokončení složení řady se provádí pomocí slova . nocases

fun const_c d = případy `Const i => i výchozí : d zábava plus_c eval d = případy `Plus (e1,e2) => eval e1 + eval e2 výchozí : d fun eval e = shoda e s const_c (plus_c eval nocases ) fun bind env v1 x v2 = if v1 = v2 then x else env v2 fun var_c env d = případy `Var v => env v default : d fun let_c eval env d = případy `Let (v,e,b) => eval (bind env v (eval env e)) b výchozí : d fun eval_var env e = shoda e s const_c (plus_c (eval_var env) (var_c env (let_c eval_var env nocases )))

Jak vidíte, nový kód, který je potřeba přidat s kvalitativní složitostí systému, nevyžaduje změnu již napsaného kódu (funkce const_ca plus_c„nic neví“ o následném přidání podpory proměnných a let-bloků do jazykový tlumočník). Prvotřídní rozšiřitelné případy jsou tedy základním řešením problému výrazu , což umožňuje mluvit o rozšiřitelném programovacím paradigmatu [71] [78] . inline polymorfismu , který je již podporován v typovém systému a v tomto smyslu je výhodou takového technického řešení jeho koncepční jednoduchost [ 34] .

Rozšíření softwarových systémů však také vyžaduje kontrolu nad zpracováním výjimek , které mohou být vyvolány v libovolné hloubce vnoření hovorů. A zde Bloom a kolegové prohlašují nový slogan pro bezpečnost typů při vývoji Milnerova sloganu : " Programy, které projdou kontrolou typu , nevyvolávají neošetřené výjimky ." Problém je v tom, že pokud podpis typu funkce obsahuje informace o typech výjimek, které může tato funkce potenciálně vyvolat, a tyto informace v podpisu předané funkce musí být přísně konzistentní s informacemi o parametru funkce vyššího řádu (včetně toto je prázdná množina ) - zadání mechanismu zpracování výjimek okamžitě vyžaduje polymorfismus typů samotných výjimek - jinak přestanou být funkce vyššího řádu polymorfní. Zároveň v bezpečném jazyce jsou výjimky rozšiřitelný součet [79] [80] [81] , tedy variantní typ, jehož konstruktory se přidávají v průběhu programu. V souladu s tím bezpečnost typu toku výjimky znamená potřebu podporovat typy součtů , které jsou rozšiřitelné i polymorfní. I zde je řešením inline polymorfismus .

Stejně jako Garriga kalkul MLPolyR používá speciální syntaxi pro polymorfní součty (backtick, úvodní značka) a není potřeba předdeklarovat typ součtu (to znamená, že výše uvedený kód je celý program, ne fragment). Výhodou je, že není problém s kontrolou úplnosti parsování: sémantika MLPolyR je definována převodem na ověřenou spolehlivost interní jazyk , který nepodporuje ani součtový polymorfismus, ani výjimky (nemluvě o nezachycených výjimkách), takže je potřeba mazání v době kompilace je samo o sobě důkazem spolehlivosti. [34]

MLPolyR využívá netriviální kombinaci několika kalkulů a dvoustupňového překladu. Využívá Remyho kalkul pro dedukce typu a shodu typu , přičemž současně využívá princip duality k reprezentaci součtů jako součinů, poté překládá jazyk do přechodného explicitně typovaného jazyka s polymorfními záznamy a poté používá účinnou kompilační metodu Ohori. . Jinými slovy, Ohoriho kompilační model byl zobecněn tak, aby podporoval Remyho kalkul [69] . Na úrovni teoretického typu zavádí Bloom několik nových syntaktických zápisů najednou, což umožňuje zapisovat pravidla pro výjimky při psaní a prvotřídní větve. Systém typu MLPolyR poskytuje úplné odvození typu , takže autoři upustili od vývoje ploché syntaxe pro explicitní psaní typů a podporu podpisů v jazyce modulu .

Systém typu Leyen také zavádí variantu polymorfismu větví: konstrukt může být reprezentován jako funkce vyššího řádu , která přijímá vstup z funkcí, z nichž každá odpovídá určitému odvětví výpočtu ( vhodná je Haskellova syntaxe pro tuto změnu a nevyžaduje revizi). Například: case

dataList a = nil :: { } | nevýhody :: { hd :: a , tl :: Seznam a } snoc xs r = případ ( reverzní xs ) r poslední xs = snoc xs { nil = \ r -> _ | _ , cons = \ r -> r . hd }

Protože záznamy v Layenově systému jsou rozšiřitelné, je analýza větví flexibilní na úrovni dynamických rozhodnutí (jako je řetězení kontrol nebo použití asociativního pole ), ale poskytuje mnohem efektivnější implementaci (označení varianty odpovídá posunu v záznamu). Výchozí podpora větvení ( default) však musí být v tomto případě zrušena, protože jeden default-pattern by odpovídal více polím (a tedy více offsetům). Leyen nazývá tuto konstrukci " prvotřídní vzory " ( prvotřídní vzory ).

Polymorfismus u vyšších rodů

Vyšší polymorfismus znamená abstrakci nad typovými konstruktory vyššího řádu, tedy typovými operátory formuláře.

* -> * -> ... -> *

Podpora této funkce posouvá polymorfismus na vyšší úroveň a poskytuje abstrakci nad typy i konstruktory typů , stejně jako funkce vyššího řádu poskytují abstrakci nad hodnotami i jinými funkcemi. Polymorfismus ve vyšších rodech je přirozenou součástí mnoha funkčních programovacích idiomů , včetně monád , záhybů a vnořitelných jazyků . [62] [82]

Například [62] , pokud definujete následující funkci ( jazyk Haskell ):

když b m = if b , pak m jinak vrátit ()

pak pro něj bude odvozen následující funkční typ :

když :: forall ( m :: * -> * ) . Monad m => Bool -> m () -> m ()

Signatura m :: * -> *říká, že typová proměnná m je typová proměnná patřící do vyššího druhu ( anglicky high-kinded type variable ). To znamená, že abstrahuje přes typové konstruktory (v tomto případě unární , jako je Maybenebo []), které lze použít na konkrétní typy, jako je Intnebo (), ke konstrukci nových typů.

V jazycích, které podporují úplnou typovou abstrakci ( Standard ML , OCaml ), musí být všechny typové proměnné rodu * , jinak by byl typový systém nebezpečný . Polymorfismus ve vyšších rodech je tedy zajištěn samotným mechanismem abstrakce v kombinaci s explicitní anotací při vytváření instance, což je poněkud nepohodlné. Idiomatická implementace polymorfismu ve vyšších rodech je však možná bez nutnosti explicitní anotace – k tomu se na typové úrovni používá technika podobná defunkcionalizaci . [62]

Generický polymorfismus

Laskavé systémy zajišťují bezpečnost samotných typových systémů tímumožňují kontrolu nad významem typových výrazů .

Nechť je například požadováno implementovat místo obvyklého typu " vector " (lineární pole) rodinu typů " length vectorn ", jinými slovy definovat typ " vector indexed by length ". Klasická implementace Haskellu vypadá takto [83] :

data Nulová data Succ n data Vec :: * -> * -> * kde Nil :: Vec a Zero Cons :: a -> Vec a n -> Vec a ( Succ n )

Zde jsou nejprve definovány fantomové typy [84] , tedy typy, které nemají dynamickou reprezentaci. Konstruktory Zero a Succslouží jako "hodnoty typové vrstvy" a proměnná nvynucuje nerovnost různých typů betonu konstruovaných konstruktorem Succ. Typ Vecje definován jako zobecněný algebraický datový typ (GADT).

Řešení podmíněně předpokládá, že fantomový typ nbude použit k modelování celočíselného parametru vektoru na základě Peanových axiomů - tedy budou sestaveny pouze výrazy jako Succ Zero, Succ Succ Zero, atd. Nicméně, ačkoli jsou definice psány v typovém jazyce Succ Succ Succ Zero, samy jsou formulovány netypizovaným způsobem. To je patrné ze signatury Vec :: * -> * -> *, což znamená, že konkrétní typy předávané jako parametry patří do rodu * , což znamená, že se může jednat o jakýkoli konkrétní typ. Jinými slovy, nesmyslné výrazy typu jako Succ Boolnebo zde nejsou zakázány Vec Zero Int. [83]

Pokročilejší výpočet by umožnil přesněji specifikovat rozsah parametru typu:

údaje Nat = nula | Succ Nat data Vec :: * -> Nat -> * kde VNil :: Vec a Zero VCons :: a -> Vec a n -> Vec a ( Succ n )

Ale takovou expresivitu mají obvykle pouze vysoce specializované systémy se závislými typy [85] implementované v jazycích jako Agda , Coq a další. Například z hlediska jazyka Agda by zápis Vec :: * -> Nat -> *znamenalo, že rod typu Vec závisí na typu Nat(to znamená, že prvek jednoho druhu závisí na prvku jiného, nižšího druhu ).

V roce 2012 bylo vybudováno rozšíření jazyka Haskell [83] , které implementuje pokročilejší systém pohlaví a činí z výše uvedeného kódu správný haskellský kód. Řešením je, že všechny typy (za určitých omezení) jsou automaticky „ povýšeny “ ( angl. promotion ) na vyšší úroveň, čímž se vytvoří stejnojmenné rody, které lze explicitně použít. Z tohoto pohledu záznam není závislý - znamená pouze, že druhý parametr vektoru musí patřit do jmenovaného rodu a v tomto případě je jediným prvkem tohoto rodu stejnojmenný typ. Vec :: * -> Nat -> *Nat

Řešení je vcelku jednoduché, jak z hlediska implementace v kompilátoru, tak z hlediska praktické dostupnosti. A protože typový polymorfismus je neodmyslitelně přirozeným prvkem Haskellovy sémantiky , propagace typu vede k laskavému polymorfismu , který zvyšuje opětovné použití kódu a poskytuje vyšší úroveň bezpečnosti typu . Například následující GADT se používá k ověření rovnosti typu:

data EqReﬂ a b kde Reﬂ :: EqReﬂ a a

má pohlaví v klasickém Haskell * -> * -> *, což brání jeho použití k testování rovnosti typových konstruktorů , jako je Maybe. Systém rodu založený na podpoře typu odvozuje polymorfní rod , díky čemuž je typ generičtější . To lze napsat explicitně: forall X. X -> X -> *EqReﬂ

data EqReﬂ ( a :: X ) ( b :: X ) kde Reﬂ :: pro všechny X . forall ( a :: X ) . EqRe ﬂ a

Polymorfismus efektů

Systémy efektů navrhli80. let [ 86] [87] [88] s cílem izolovat vedlejší efekty pro jemnější kontrolu nad bezpečností a účinností v konkurenčním programování .

V tomto případě polymorfismus efektu znamená kvantifikaci čistoty specifické funkce , to znamená zahrnutí příznaku do funkčního typu , který charakterizuje funkci jako čistou nebo nečistou. Toto rozšíření pro psaní umožňuje abstrahovat čistotu funkcí vyššího řádu od čistoty funkcí, které jim byly předány jako argumenty.

To je zvláště důležité při přechodu na funkce přes moduly ( záznamy , které obsahují abstraktní typy ) - funktory - protože v podmínkách čistoty mají právo být aplikovatelné, ale za přítomnosti vedlejších účinků musí být generovány, aby byla zajištěna bezpečnost typu (více o tom viz ekvivalence typů v jazyce modulu ML ). V jazyce prvotřídních modulů vyššího řádu se tedy efektový polymorfismus ukazuje jako nezbytný základ pro podporu generativního polymorfismu : předání příznaku čistoty funktoru poskytuje volbu mezi aplikační a generativní sémantikou v jediném systému. [65]

Podpora v programovacích jazycích

Typově bezpečný parametrický polymorfismus je dostupný v Hindley-Milner -typovaných jazycích — v dialektech ML ( Standard ML , OCaml , Alice , F# ) a jejich potomcích ( Haskell , Clean , Idris , Mercury , Agda ) — také jako v těch, které od nich zdědily hybridní jazyky ( Scala , Nemerle ).

Generické datové typy (generika) se od parametricky polymorfních systémů liší tím, že používají omezenou kvantifikaci , a proto nemohou mít vyšší rank než 1 . Jsou k dispozici v Ada , Eiffel , Java , C# , D , Rust ; a také v Delphi od verze 2009. Poprvé se objevili v CLU .

Intenzionální polymorfismus

Intenzionální polymorfismus je technika optimalizace kompilace parametrického polymorfismu založená na komplexní typově teoretické analýze, která spočívá ve výpočtech typů za běhu. Intenzionální polymorfismus umožňuje shromažďování odpadků bez značek, předávání argumentů funkcím bez rámečků a ploché datové struktury v krabicích (optimalizované pro paměť). [89] [90] [91]

Monomorfizace

Monomorfizace je technika pro optimalizaci kompilace parametrického polymorfismu, která spočívá ve generování monomorfní instance prokaždý případ použití polymorfní funkce nebo typu. Jinými slovy, parametrický polymorfismus na úrovni zdrojového kódu se převádí na ad hoc polymorfismus na úrovni cílové platformy. Monomorfizace zlepšuje výkon (přesněji řečeno činí polymorfismus „volným“), ale zároveň může zvětšit velikost výstupního strojového kódu . [92]

Hindley - Milner

V klasické verzi je systém typu Hindley-Milner (také jednoduše "Hindley-Milner" nebo "X-M", anglicky HM ) [93] [94] , který je základem jazyka ML podmnožinou systému F , omezený predikativním prenex polymorfismus umožňující automatické odvozování typu , pro který Hindley-Milner tradičně zahrnoval také takzvaný „ Algorithm W “ , vyvinutý Robinem Milnerem .

Mnoho implementací X-M je vylepšenou verzí systému, která představuje „ hlavní typizační schéma “ [93] [2] , které v jediném průchodu s téměř lineární složitostí současně odvozuje nejobecnější polymorfní typy pro každý výraz a přísně kontroluje jejich dohoda .

Systém typu Hindley-Milner byl od svého vzniku rozšířen několika způsoby [95] . Jedním z nejznámějších rozšíření je podpora ad-hoc polymorfismu prostřednictvím typových tříd , které se dále zobecňují na kvalifikované typy .

Automatická inference typu byla považována za nezbytnost v původním vývoji ML jako interaktivního systému pro dokazování teorémů „ Logika pro výpočetní funkce “, a proto byla uvalena odpovídající omezení. Následně byla na základě ML vyvinuta řada efektivně kompilovaných univerzálních jazyků orientovaných na rozsáhlé programování , a v tomto případě je potřeba podpory typové inference výrazně omezena, protože modulová rozhraní v průmyslové praxi musí být v každém případě výslovně označeny typy [81] . Proto bylo navrženo mnoho Hindley-Milnerových rozšíření, která se vyhýbají inferenci typu ve prospěch zmocnění, až do a včetně podpory pro kompletní systém F s nepředvídatelným polymorfismem, jako je modulový jazyk vyššího řádu , který byl původně založen na explicitní anotace typu modulu a má mnoho rozšíření a dialektů, stejně jako rozšíření jazyka Haskell ( , a ). Rank2TypesRankNTypesImpredicativeTypes

Kompilátor MLton standardu ML monomorfizuje , ale kvůli jiným optimalizacím použitelným pro Standard ML výsledné zvýšení výstupního kódu nepřesáhne 30 % [92] .

C a C++

V C nejsou funkce prvotřídními objekty , ale je možné definovat ukazatele funkcí , což umožňuje sestavit funkce vyšších řádů [96] . Nebezpečný parametrický polymorfismus je také dostupný explicitním předáním požadovaných vlastností typu přes netypizovanou podmnožinu jazyka reprezentovaného netypovým ukazatelem ).“ukazatel generickýnazývaný „komunitěv97][ polymorfismus ad-hoc , protože nemění reprezentaci ukazatele, je však napsán výslovně tak, aby obešel typový systém kompilátoru [96] . void* void*

Standardní funkce qsortje například schopna zpracovat pole prvků libovolného typu, pro které je definována porovnávací funkce [96] .

struct segment { int start ; int konec ; }; int seg_cmpr ( struct segment * a , struct segment * b ) { return abs ( a -> konec - a -> začátek ) - abs ( b -> konec - b -> začátek ); } int str_cmpr ( char ** a , char ** b ) { return strcmp ( * a , * b ); } struct segment segs [] = { { 2 , 5 }, { 4 , 3 }, { 9 , 3 }, { 6 , 8 } }; char * strs [] = { "tři" , "jedna" , "dva" , "pět" , "čtyři" }; hlavní () { qsort ( strs , sizeof ( strs ) / sizeof ( char * ), sizeof ( char * ), ( int ( * )( void * , void * )) str_cmpr ); qsort ( segs , sizeof ( segs ) / sizeof ( struct segment ), sizeof ( struct segment ), ( int ( * )( void * , void * )) seg_cmpr ); ... }

V C je však možné idiomaticky reprodukovat typovaný parametrický polymorfismus bez použití void*[98] .

Jazyk C++ poskytuje šablonový subsystém , který vypadá jako parametrický polymorfismus, ale je sémanticky implementován kombinací ad hoc mechanismů:

šablona < název typu T > T max ( T x , T y ) { pokud ( x < y ) vrátit y ; jiný návrat x ; } int main () { int a = max ( 10 , 15 ); dvojité f = max ( 123,11 , 123,12 ); ... }

Monomorfizaci při kompilaci šablon C++ se nelze vyhnout , protože typový systém jazyka postrádá podporu pro polymorfismus - polymorfní jazyk je zde statickým doplňkem k jádru monomorfního jazyka [99] . To vede k mnohonásobnému zvýšení množství přijímaného strojového kódu , což je známé jako „ code bloat “ [100] .

Historie

Zápis parametrického polymorfismu jako vývoje lambda kalkulu (nazývaného polymorfní lambda kalkul nebo Systém F ) formálně popsal logik Jean-Yves Girard [101] [102] ( 1971 ), nezávisle na něm podobný systém popsal počítačový vědec John S. Reynolds [103] ( 1974 ) [104] .

Parametrický polymorfismus byl poprvé zaveden v ML v roce 1973 [41] [105] . Nezávisle na něm byly implementovány parametrické typy pod vedením Barbary Liskov na CLU ( 1974 ) [41] .

Viz také

Poznámky

↑ 1 2 Strachey, "Základní koncepty", 1967 .
↑ 1 2 Pierce, 2002 .
↑ Cardelli, Wegner, „On Understanding Types“, 1985 , 1.3. Druhy polymorfismu, str. 6.
↑ 1 2 Appel, "Critique of SML", 1992 .
↑ 1 2 Jones, "Teorie kvalifikovaných typů", 1992 .
↑ 1 2 3 4 5 6 7 Gaster, Jones, "Polymorphic Extensible Records and Variants", 1996 .
↑ Cardelli, "Basic Polymorphic Typechecking", 1987 .
↑ 1 2 Wonseok Chae (Ph.D. Diplomová práce), 2009 , s. 91-92.
↑ 1 2 3 4 5 6 Rossberg, "1ML - Core and Modules United (F-ing First-class Modules)", 2015 .
↑ Blume, "Osoby výjimek", 2008 , str. jedenáct.
↑ Wells, 1994 .
↑ Pierce, 2002 , 22 Rekonstrukce typů, str. 361.
↑ Pierce, 2002 , 23.6 Výmaz, typizace a rekonstrukce typu, str. 378-381.
↑ Remy, "ML s abstrakty a typy záznamů", 1994 .
↑ Garrigue, Remy, "Semi-Explicit First-Class Polymorphism for ML", 1997 .
↑ Reynolds, "Teorie programovacích jazyků", 1998 , 17. Polymorfismus. Bibliografické poznámky, str. 393.
↑ Prvotřídní polymorfismus na MLton . Získáno 28. července 2016. Archivováno z originálu dne 28. listopadu 2015. (neurčitý)
↑ Pierce, 2002 , 22.7 Polymorphism via let, str. 354-359.
↑ 1 2 3 4 5 Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 .
↑ Dushkin, „Monomorfismus, polymorfismus a existenciální typy“, 2010 .
↑ Cardelli, "Typové programování", 1991 , s. dvacet.
↑ Pierce, 2002 , 23.10 Nepředvídatelnost, str. 385.
↑ Pierce, 2002 , Kapitola 22. Rekonstrukce typu. Část 22.8. Další poznámky, str. 361-362.
↑ Wonseok Chae (Ph.D. Diplomová práce), 2009 , s. čtrnáct.
↑ 1 2 3 Garrigue, "Polymorfní varianty", 1998 .
↑ Blume, "Rozšiřitelné programování s prvotřídními případy", 2006 , str. deset.
↑ 1 2 3 4 5 6 7 8 9 Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , 1.1 Static Type System for Record Polymorphism, str. 3-6.
↑ Leijen, "Prvotřídní etikety", 2004 , s. jeden.
↑ Gaster, Jones, "Polymorphic Extensible Records and Variants", 1996 , Abstrakt, str. jeden.
↑ 1 2 Paulson, "ML for the Working Programmer", 1996 , 2.9 Records, str. 35.
↑ 1 2 3 4 Ohori, "Polymorphic Record Calculus and its Compilation", 1995 , 1.2 Compilation Method for Record Polymorphism, str. 6-8.
↑ Harper, „Úvod do SML“, 1986 .
↑ 1 2 3 Remy, "Type Inference for Records", 1991 , str. 2.
↑ 1 2 3 4 5 Blume, "Řádkový polymorfismus při práci", 2007 .
↑ Aktualizace funkčních záznamů . Získáno 30. června 2016. Archivováno z originálu 2. června 2016. (neurčitý)
↑ 1 2 Syntaktická vylepšení Alice ML . Získáno 30. června 2016. Archivováno z originálu 27. listopadu 2016. (neurčitý)
↑ Funkční rozšíření záznamu a zachycení řádků . Získáno 30. června 2016. Archivováno z originálu 13. srpna 2016. (neurčitý)
↑ Harper, Pierce, "Record calculus based on symmetric concatenation", 1991 .
↑ 1 2 Hůlka, "Odvozování typů pro zřetězení záznamů a vícenásobnou dědičnost", 1991 .
↑ 12 Sulzmann , 1997 .
↑ 1 2 3 4 Pierce, 2002 , 1.4 Stručná historie, str. 11-13.
↑ Remy, "Type Inference for Records", 1991 , str. 2-3.
↑ 1 2 3 4 5 6 7 Leijen, "First-class Labels", 2004 , str. 13-14.
↑ Cardelli, "Sémantika vícenásobné dědičnosti", 1988 .
↑ Cardelli, Wegner, "On Understanding Types", 1985 .
↑ Pierce, 2002 , 16. Subtypová metateorie, str. 225.
↑ Pierce, 2002 , 11.8 Nahrávky, str. 135.
↑ 1 2 3 Minsky přeložil DMK, 2014 , Subtyping and inline polymorphism, str. 267-268.
↑ Hůlka, "Type inference for objects", 1987 .
↑ 1 2 Minsky přeložil DMK, 2014 , Polymorfismus objektů, str. 255-257.
↑ 1 2 Remy, "Type Inference for Records", 1991 , Související práce, str. 3.
↑ 1 2 Remy, "Type Inference for Records", 1991 .
↑ Blume, "Rozšiřitelné programování s prvotřídními případy", 2006 , str. jedenáct.
↑ Remy, "Subtypes and Row polymorphism", 1995 .
↑ 1 2 Remy, Vouillon, "Objective ML", 1998 .
↑ Pierce, 2002 , 15.8 Další poznámky, str. 223.
↑ Minsky přeložil DMK, 2014 , Polymorfní varianty, str. 149-158.
↑ Pierce, 2002 , 24 existenciálních typů, str. 404.
↑ 1 2 Reynolds, "Teorie programovacích jazyků", 1998 , 18. Module Specification, s. 401-410.
↑ Cardelli, "Typové programování", 1991 , 4.4. Typy tuple, str. 20-23.
↑ 1 2 Harper, Lillibridge, "Typově teoretický přístup k modulům vyššího řádu se sdílením", 1993 .
↑ 1 2 3 4 Yallop, White, "Lehký polymorfismus vyššího druhu", 2014 .
↑ Harper, Mitchell, "Type Structure of SML", 1993 .
↑ Rossberg, "1ML - Core and Modules United (F-ing First-class Modules)", 2015 , Impredicativity Reloaded, str. 6.
↑ 1 2 Rossberg, "1ML se speciálními efekty (F-ing Generativity Polymorphism)", 2016 .
↑ Ohori, "Compilation Method for Polymorphic Record Calculi", 1992 .
↑ Ohori - SML# (prezentace) (downlink) . Získáno 30. června 2016. Archivováno z originálu 27. srpna 2016. (neurčitý)
↑ Ohori, "Polymorfní záznamový počet a jeho kompilace", 1995 , s. 38.
↑ 1 2 Blume, "Rozšiřitelné programování s prvotřídními případy", 2006 , str. 9.
↑ Ohori, "Polymorphic Record Calculus and its Compilation", 1995 , 5 Implementaion, s. 37.
↑ 1 2 3 4 5 Blume, "Rozšiřitelné programování s prvotřídními případy", 2006 .
↑ Gaster (Ph.D. Diplomová práce), 1998 .
↑ Leijen, "Prvotřídní etikety", 2004 , s. 7.
↑ Leijen, "Prvotřídní etikety", 2004 .
↑ Rozšiřitelné záznamy na Haskell-Wiki (downlink)
↑ Osobní stránka Blume . Získáno 30. června 2016. Archivováno z originálu 19. května 2016. (neurčitý)
↑ Blume, "Osoby výjimek", 2008 .
↑ 1 2 3 Wonseok Chae (Ph.D. práce), 2009 .
↑ Paulson, "ML for the Working Programmer", 1996 , 4.6 Declaring Výjimky, str. 135.
↑ Harper, "Practical Foundations for Programming Languages", 2012 , 28.3 Typ výjimky, str. 258-260.
↑ 1 2 Předběžný návrh ML2000, 1999 .
↑ Harper, "Practical Foundations for Programming Languages", 2012 , kapitola 22. Konstruktory a druhy, str. 193.
↑ 1 2 3 Weirich et al, „Giving Haskell a promotion“, 2012 .
↑ Flétna, Pucella, "Fantomové typy a podtypování", 2006 .
↑ Pierce, 2002 , 30.5 Jít dále: závislé typy, str. 489-490.
↑ Gifford, Lucassen, "Efektové systémy", 1986 .
↑ Lucassen, Gifford, "Polymorphic Effect Systems", 1988 .
↑ Talpin, Jouvelot, 1992 .
↑ Harper, Morrisett, "Intensional Type Analysis", 1995 .
↑ Crary, Weirich, Morrisett, "Intenzionální polymorfismus", 1998 .
↑ Pierce, 2002 , 23.2 Variety polymorfismu, s. 364-365.
↑ 1 2 týdny, "Kompilace celého programu v MLton", 2006 .
↑ 1 2 Hindley, "Principal Type Scheme", 1969 .
↑ Milner, "Teorie typového polymorfismu", 1978 .
↑ Jones, "FP with Overloading and HO Polymorphism", 1995 .
↑ 1 2 3 Kernighan B. , Ritchie D. Programovací jazyk C = Programovací jazyk C. - 2. vyd. - Williams , 2007. - S. 304. - ISBN 0-13-110362-8 . , kapitola 5.11. Ukazatele funkcí
↑ Appel, "Kritika SML", 1992 , s. 5.
↑ Oleg Kiseljov. Skutečně polymorfní seznamy v C . okmij.org. Získáno 22. listopadu 2016. Archivováno z originálu 30. ledna 2017. (neurčitý)
↑ Mitchell, "Koncepty v programovacích jazycích", 2004 , 6.4. Polymorfismus a přetěžování, str. 145-151.
↑ Scott Meyers . Kód nafouklý kvůli šablonám . comp.lang.c++.moderováno . Usenet (16. května 2002). Staženo: 19. ledna 2010. (neurčitý)
↑ Girard, "Extension of Type Theory", 1971 .
↑ Girard, "Výpočet vyššího řádu", 1972 .
↑ Reynolds, "Teorie typové struktury", 1974 .
↑ Pierce, 2002 , 23.3 System F, s. 365-366.
↑ Milner a kol., "LCF", 1975 .

Literatura

Christopher Strachey. Základní pojmy v programovacích jazycích . - 1967. Archivováno 12. srpna 2017.
- Znovu publikováno: Christopher Strachey. Základní pojmy v programovacích jazycích // Vyšší řád a symbolické výpočty . - 2000. - T. 13 . - S. 11-49 . - doi : 10.1023/A:1010000313106 .

J Roger Hindley. Hlavní typové schéma objektu v kombinační logice // Transactions of the American Mathematical Society . - Americká matematická společnost, 1969. - Sv. 146 . - str. 29-60 . - doi : 10.2307/1995158 .

Jean-Yves Girard. Une Extension de l'Interpretation de l'Interpretation de Gödel à l'Analyse, et son Application à l'Elimination des Coupures dans l'Analyse et la Théorie des Types (francouzsky) // Sborník z druhého sympozia skandinávské logiky. - Amsterdam, 1971. - S. 63-92 . - doi : 10.1016/S0049-237X(08)70843-7 .

Jean-Yves Girard. Interprétation fonctionnelle et elimination des coupures de l'arithmétique d'ordre supérieur (francouzsky) . — Université Paris 7, 1972.

John C. Reynolds. Towards a Theory of Type Structure // Poznámky k přednáškám z informatiky . - Paříž: Colloque sur la programmation, 1974. - svazek 19 . - S. 408-425 . - doi : 10.1007/3-540-06859-7_148 .

Milner R. , Morris L., Newey M. Logika pro vyčíslitelné funkce s reflexivními a polymorfními typy // Arc-et-Senans. — Proc. Konference o ověřování a zlepšování programů, 1975.

Robin Milner . Teorie typového polymorfismu v programování. - Journal of Computer and System Sciences , 1978. - V. 17 , no. 3 . - S. 348-375 . - doi : 10.1016/0022-0000(78)90014-4 .

Luca Cardelli , John C. Mitchell. Operace se záznamy // Matematické struktury v informatice. - 1991. -1,vydání. 1.

Luca Cardelli , Peter Wegner. O porozumění typům, abstrakci dat a polymorfismu //ACM Computing Surveys. - New York, USA:ACM, 1985. -17,č. 4. -S. 471-523. —ISSN 0360-0300. -doi:10.1145/6041.6042.

Robert Harper . Úvod do standardního ML. - Carnegie Mellon University, 1986. - 97 s. — ISBN PA 15213-3891. (Ruština)

John M. Lucassen, David K. Gifford. Integrace funkcionálního a imperativního programování . — 1986.

Luca Cardelli . Základní polymorfní typová kontrola. — 1987.

Mitchell Wand . Kompletní odvození typu pro jednoduché objekty // In Proc. 2nd IEEE Symposium on Logic in Computer Science. - 1987. -S. 37-44.

Martín Abadi, Luca Cardelli , Pierre-Louis Curien. Formální parametrický polymorfismus . — POPL, 1993.

Luca Cardelli . A Sémantika vícenásobné dědičnosti // Inf. Počítat. 76. - 1988. -S. 138-164.

John M. Lucassen, David K. Gifford. Polymorfní efektové systémy . — POPL , 1988.

Didier Remy. Typová inference pro záznamy v přirozeném rozšíření ML // Research Report 1431. - Institut National de Recherche en Informatique et Automatisme, 1991.

Luca Cardelli . Typické programování // Zprávy IFIP o stavu umění. - New York: Springer-Verlag, 1991. -Iss. Formální popis programovacích konceptů. -S. 431-507.

Robert Harper , Benjamin Pierce. Záznamový počet založený na symetrickém zřetězení // CMU-CS-90-157R. — Univerzita Carnegie Mellon, podporovaná a monitorovaná společností Naval Research, 1991.

Mitchell Wand . Typová inference pro zřetězení záznamů a vícenásobnou dědičnost // Výběr z 1989 IEEE Symposium on Logic in Computer Science. - Informace a výpočty, 1991. -T. 93,no. 1. -doi:10.1016/0890-5401(91)90050-C.

Andrew W. Appel. Kritika standardního ML . — Princetonská univerzita, 1992.

Mark P. Jones. Teorie kvalifikovaných typů . — ESOP , Springer-Verlag Lecture Notes in Computer Science, 1992.

Atsushi Ohori. A Compilation Method for ML-Style Polymorphic Record Calculi // POPL: Sborník příspěvků z 19. sympozia ACM SIGPLAN-SIGACT o principech programovacích jazyků,. - Kyoto University, ACM , 1992. - S. 154-165 . - doi : 10.1.1.105.7655 .

J.P. Talpin, P. Jouvelot. Polymorfní typ, oblast a odvození účinku // 2(3):245271. — JFP , 1992.

Robert Harper , John C. Mitchell. O typové struktuře standardního ML. -ACMTOPLAS, 1993. -S. 211-252.

Robert Harper , Mark Lillibridge. Typově teoretický přístup k modulůmse sdílením . -ACMPress,POPL, 1993. - ISBN CMU-CS-93-197. -doi:10.1.1.14.3595.

Didier Remy. Programování objektů pomocí ML-ART: Rozšíření ML s abstraktními a záznamovými typy . - Mezinárodní symposium o teoretických aspektech počítačového softwaru, Springer-Verlag, 1994. - S. 321-346 .

JB Wells. Typovatelnost a kontrola typu v lambda-kalkulu druhého řádu jsou ekvivalentní a nerozhodnutelné // Proceedings of the 9th Annual IEEE . - Symposium on Logic in Computer Science (LIS), 1994. - S. 176-185 .

Robert Harper , . Kompilace polymorfismu pomocí intenzionální typové analýzy. — 1995.

Atsushi Ohori. Polymorfní záznamový počet a jeho kompilace . - Kyoto University, ACM , 1995. - S. 844-895 .

Mark P. Jones. Funkční programování s přetížením a polymorfismem vyššího řádu . - Springer-Verlag Lecture Notes, 1995. - doi : 10.1.1.26.9460 .

Didier Remy. Lepší podtypy a proměnné řádků pro typy záznamů // Prezentováno na workshopu Pokroky v typech pro informatiku v Newton Institute. — Cambridge, Velká Británie, 1995.

Lawrence C. Paulson . ML pro pracujícího programátora. — 2. - Cambridge, Velká Británie: Cambridge University Press, 1996. - 492 s. -ISBN 0-521-57050-6(pevná vazba), 0-521-56543-X (brožovaná).

Benedict R. Gaster, Mark P. Jones. Systém polymorfního typu pro rozšiřitelné záznamy a varianty // Technická zpráva NOTTCS-TR-96-3. — University of Nottingham, 1996.

Jacques Garrigue, Didier Remy. Poloexplicitní prvotřídní polymorfismus pro ML // Academic Press. — Informace a výpočty, 1997.

M. Sulzmann. Navrhování záznamových systémů // Technická zpráva YALEU/DCS/RR-1128. - Yale University, 1997. - doi : 10.1.1.17.6563 .

Karl Crary, Stephanie Weirich, J. Gregory Morrisett. Intenzionální polymorfismus v sémantice typového výmazu . — ICFP , 1998.

Benedict R. Gaster. Záznamy, varianty a kvalifikované typy // Technická zpráva NOTTCS-TR-98-3. — Ph.D. Diplomová práce, 1998.

Jacques Garrigue. Programování s polymorfními variantami . — Univerzita v Kjótu, 1998.

Didier Rémy, Jérome Vouillon. Objective ML: Efektivní objektově orientované rozšíření ML . - Teorie a praxe objektových systémů, ACM , 1998. - V. 4 (1) . - S. 27-50 .

John C. Reynolds. Teorie programovacích jazyků . - Cambridge University Press, 1998. - ISBN 978-0-521-59414-1 (pevná vazba), 978-0-521-10697-9 (brožovaná).

Pracovní skupina ML2000. Principy a předběžný návrh pro ML2000 . — 1999.

Benjamin Pierce. Typy a programovací jazyky . - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Překlad do ruštiny: Benjamin Pierce. Typy v programovacích jazycích. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .

John C. Mitchell Pojmy v programovacích jazycích. - Cambridge University Press, 2004. - ISBN 0-511-04091-1 (elektronická kniha v netLibrary); 0-521-78098-5 (pevná vazba).

Jens Palsberg, Tian Zhao. Zadejte odvození pro zřetězení záznamů a podtypování . - 2004. Archivováno 16. září 2016.

Daan Leijen. Prvotřídní štítky pro rozšiřitelné řádky // TechReport UU-CS-2004-51. — Universiteit Utrecht, 2004.

Matthias Blume, Umut A. Acar, Wonseok Chae. Rozšiřitelné programování s prvotřídními případy . — ICFP , 2006.

Matthew Fluet, Riccardo Pucella. Fantomové typy a podtypování . — JFP , 2006.

Stephen Weeks. Kompilace celého programu v MLton . - 2006. Archivováno 29. června 2007.

Matyáš Blume. Záznamy, součty, případy a výjimky: Polymorfismus řádků v práci : video řeči. — Microsoft, 2007.

Matthias Blume, Umut A. Acar, Wonseok Chae. Obslužné rutiny výjimek jako rozšiřitelné případy . - Toyota Technologický institut v Chicagu, APLAS, 2008.

Wonseok Chae. Typ Safe Extensible Programming // Ph.D. teze. — Toyota Technologický institut v Chicagu, 2009.

Roman Dushkin. Monomorfismus, polymorfismus a existenciální typy . — 2010.

Jeremy Yallop, Leo White. Lehký polymorfismus vyššího druhu . — Mezinárodní symposium o funkcionálním a logickém programování, 2014.

Robert Harper . Praktické základy programovacích jazyků. - verze 1.37 (revidováno 1. 11. 2014). - pod licencí Creative Commons Attribution-Nonkomerční-No Derivative Works 3.0 United States License., 2012. - 544 s. Archivováno24. října 2015 naWayback Machine

Stephanie Weirich, Brent A. Yorgey, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis a Jose P. Magalhães. Povýšení Haskell // In Proceedings of 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation. - NY, USA: TLDI , 2012. - S. 53-66 .

Minsky, Madhavapeddy, Hickey. Skutečný svět OCaml: Funkční programování pro masy . - O'Reilly Media, 2013. - 510 s. — ISBN 9781449324766 .
- Překlad do ruštiny:
  Minsky, Madhavapeddy, Hickey. Programování v jazyce OCaml . - DMK, 2014. - 536 s. - ISBN 978-5-97060-102-0 . (Ruština)

Andreas Rossberg. 1ML - Core and Modules United (F-ing First Class Modules) . — ICFP , 2015.

Andreas Rossberg. 1ML se speciálními efekty (F-ing Generativity Polymorphism) . — WadlerFest, Google, 2016.

Haskell-Wiki: Existenciální typy . (neurčitý)

Haskell-Wiki: Rank-N typy . (neurčitý)

Haskell-Wiki: Nepredikativní typy . (neurčitý)

Jacques Garrigue. OCaml manuál: Polymorfní varianty . (neurčitý)

Typy dat
Neinterpretovatelné	Bit Okusovat Byte qubit Zacházet Vlastnost Slovo
Numerický	Celý pevný bod plovoucí bod Racionální Komplex Dlouho časový úsek
Text	Symbolický Tětiva
Odkaz	Adresa Odkaz Ukazatel Obal
Kompozitní	Algebraický datový typ ( generický ) Třída Typový produkt ( Write Tuple struktura ) Objekt Konsolidace ( označeno ) Objednaný pár
abstraktní	pole Seznam Otočit se Zásobník Asociativní pole (displej, mapa ) Hodně multiset Typ Graf
jiný	Logický Dolní Vyšší Polymorfní Funkční spočítatelný Sbírka Výjimka Rod ( metatřída ) Monad Semafor Tok prázdnota
související témata	Abstraktní datový typ primitivní typ Datová struktura Obecný typ proměnné Rozhraní Konstruktor (OOP) konstruktér (FP) Typový konstruktor Typové odlévání Prototyp Typový systém