Paraméteres polimorfizmus

Az oldal jelenlegi verzióját még nem ellenőrizték tapasztalt közreműködők, és jelentősen eltérhet a 2021. április 12-én felülvizsgált verziótól ; az ellenőrzések 5 szerkesztést igényelnek .

A paraméteres polimorfizmus a programozási nyelvekben és a típuselméletben a típusrendszer szemantikájának olyan tulajdonsága, amely lehetővé teszi a különböző típusú értékek azonos módon történő feldolgozását, azaz ugyanazon kód fizikai végrehajtását a különböző típusú adatokhoz. [1] [2] .

A paraméteres polimorfizmust a polimorfizmus "igazi" formájának tekintik [3] , ami kifejezőbbé teszi a nyelvet, és jelentősen növeli a kód újrafelhasználását . Hagyományosan szemben áll az ad-hoc-polimorfizmussal [1] , amely egyetlen interfészt biztosít az adott kontextusban engedélyezett, potenciálisan inkompatibilis ( statikusan vagy dinamikusan ) különböző típusú kódokhoz . Számos számításban, például a minősített típusok elméletében , az ad-hoc polimorfizmust a parametrikus polimorfizmus speciális eseteként kezelik.

A paraméteres polimorfizmus az ML család nyelvtípusrendszereinek hátterében ; az ilyen típusú rendszereket polimorfnak nevezzük. A nem polimorf típusú rendszerekkel rendelkező nyelvek közösségeiben ( Algol és BCPL [4] leszármazottai ) a parametrikusan polimorf függvényeket és típusokat " általánosítottnak " nevezik .

Típuspolimorfizmus

A " paraméteres polimorfizmus " kifejezést hagyományosan a típusbiztos parametrikus polimorfizmusra használják, bár ennek tipizálatlan formái is léteznek (lásd parametrikus polimorfizmus C és C++ nyelven ) [4] . A típusbiztos parametrikus polimorfizmus kulcsfogalma a polimorf függvény mellett a polimorf típus .

A polimorf típus ( eng. polymorphic type ), vagy a politípus ( eng. polytype ) egy másik típus által paraméterezett típus. A típusrétegben lévő paramétert típusváltozónak (vagy típusváltozónak) nevezzük.

Formálisan a típuspolimorfizmust a polimorfikusan tipizált lambda kalkulusban , az F -nek nevezett rendszerben vizsgálják.

Például egy függvény, amely appendkét listát egybe fűz , a listaelemek típusától függetlenül építhető fel. A típusváltozó írja a le a listaelemek típusát . Ezután a függvény appendbegépelhető a következővel: " forall a. [a] × [a] -> [a]" (itt a konstrukció [a]azt jelenti, hogy " egy lista, amelynek minden eleme rendelkezik egy típussala " - a Haskell nyelvben elfogadott szintaxis ). Ebben az esetben a típusról azt mondjuk, hogy aminden értékhez egy változó paraméterezi a. appendAz adott argumentum minden alkalmazási helyén az érték afeloldásra kerül, és minden egyes említése az típusú aláírásban az alkalmazás kontextusának megfelelő értékre kerül. Ebben az esetben tehát a függvénytípus -aláírás megköveteli, hogy mindkét lista elemtípusa és az eredmény azonos legyen.

A típusváltozó érvényes értékeinek halmazát kvantifikáció adja meg . A legegyszerűbb kvantorok univerzálisak (mint a példában append) és egzisztenciálisak (lásd alább).

A minősített típus egy polimorf típus, amely emellett predikátumkészlettel van felszerelve, amelyek szabályozzák az ilyen típusú paraméterek érvényes értékeinek tartományát. Más szóval, a típusminősítés lehetővé teszi a számszerűsítés tetszőleges módon történő vezérlését. A minősített típusok elméletét Mark P. Jones építette fel 1992 -ben [5] . Közös indoklást biztosít a legegzotikusabb típusrendszerekhez, ideértve a típusosztályokat , bővíthető jelöléseketés altípusokat , és lehetővé teszi specifikus megszorítások pontos megfogalmazását az adott polimorf típusokhoz, így megteremtve a kapcsolatot a parametrikus és az ad-hoc között. polimorfizmus ( túlterhelés ), valamint az explicit és az implicit túlterhelés között. Egy típus predikátummal való társítását ebbenaz elméletben bizonyítéknak nevezzük . A lambda-számításhoz hasonló algebrát , beleértve a bizonyítékok absztrakcióját, a bizonyítékok alkalmazását stb. Az algebra egy tagjának egy kifejezetten túlterhelt függvénnyel való korrelációját bizonyítékfordításnak nevezzük .

Az általánosított elmélet kidolgozásának motiváló példái a Wadler-Blott típusú osztályok és a bővíthető rekordok Harper-Pearce predikátumokon keresztül történő tipizálása [5] [6] .

Polimorf rendszerek osztályozása

A paraméteresen polimorf típusú rendszereket alapvetően a rang és a predikatív tulajdonság alapján osztályozzuk . Ezen kívül megkülönböztetünk explicit és implicit polimorfizmust [7] és számos más tulajdonságot. Az implicit polimorfizmust típuskövetkeztetés biztosítja , ami nagymértékben javítja a használhatóságot, de korlátozott kifejezőképességgel. Sok gyakorlati paraméteresen polimorf nyelv elválasztja egy külső implicit módon tipizált nyelv és egy belső , kifejezetten tipizált nyelv fázisait .

A polimorfizmus legáltalánosabb formája a „ magasabb rangú impredikatív polimorfizmus ”. Ennek a formának a legnépszerűbb megkötései az 1. rangú polimorfizmus , az úgynevezett " prenex " és a predikatív polimorfizmus . Ezek együtt " predikatív prenex polimorfizmust " alkotnak , hasonlóan az ML - ben és a Haskell korábbi verzióiban megvalósítotthoz .

A típusrendszerek bonyolultabbá válásával a típusaláírások olyan bonyolulttá válnak, hogy teljes vagy csaknem teljes levezetésüket sok kutató kritikus tulajdonságnak tekinti, amelynek hiánya a nyelvet a gyakorlatban alkalmatlanná teszi [8] [9] . Például egy hagyományos kombinátor esetében a teljes típusú aláírás (az általános kvantifikáció mapfigyelembevételével ) a típusbiztos kivételfolyamkövetés alatt a következő formában jelenik meg [10] [8] (mint fent , a típusú elemek ):[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 {\xrightarrow {\gamma }}\beta \;)\;{\xrightarrow {\delta }}\;(\;\left[\alpha \ jobbra]{\xrightarrow {\gamma }}\left[\beta \right]\;)$

Rang

A polimorfizmus rangja a rendszer keretein belül megengedett típusú változók kvantorainak egymásba ágyazási mélységét. A " k rangú polimorfizmus " ( k > 1 esetén ) lehetővé teszi, hogy típusváltozókat adjon meg a ( k -1) -nél nem magasabb rangú polimorf típusok szerint. A " magasabb rangú polimorfizmus " lehetővé teszi, hogy a típusú változók kvantorait tetszőleges számú nyíltól balraa magasabb rendű típusokban .

Joe Wells bebizonyította [ 11] , hogy a Curry-típusú System F típuskövetkeztetés nem dönthető el 2 - nél magasabb rangoknál, ezért explicit típusannotációt kell használni magasabb rangok használatakor [12] .

Léteznek részleges következtetéses típusú rendszerek , amelyekhez csak a nem levezethető típusú változókat kell annotálni [13] [14] [15] .

Prenex polimorfizmus

Az 1. rangú polimorfizmust gyakran prenex polimorfizmusnak nevezik (a "prenex" szóból - lásd a prenex normál alakját ). Egy prenex polimorf rendszerben a típusváltozók nem példányosíthatók polimorf típusokkal. Ez a korlát elengedhetetlenné teszi a monomorf és polimorf típusok megkülönböztetését, ezért a prenex rendszerben a polimorf típusokat gyakran " tipizálási sémáknak " ( angol típussémáknak ) nevezik, hogy megkülönböztessük őket a "hétköznapi" (monomorf) típusoktól (monotípusoktól). Következésképpen minden típus felírható olyan formában, amikor minden típusú változó kvantor a legkülső (prenex) pozícióba kerül, amit prenex normál alaknak nevezünk . Egyszerűen fogalmazva, a polimorf függvények definíciói megengedettek, de a polimorf függvények nem adhatók át argumentumként más függvényeknek [16] [17] – a polimorf módon definiált függvényeket használat előtt monotípus példányosítani kell.

Ennek közeli megfelelője Damas-Milner úgynevezett " Let-polimorfizmusa " vagy " ML - stílusú polimorfizmusa ". Technikailag a Let-polimorfizmus az ML -ben további szintaktikai megszorításokkal rendelkezik, például a hivatkozások használatakor a típusbiztonsági problémákhoz kapcsolódó " értékkorlátozás " (amelyek nem fordulnak elő olyan tiszta nyelvekben, mint a Haskell és a Clean ) [18] [19] .

Predikativitás

Predikatív polimorfizmus

A predikatív (feltételes) polimorfizmus megköveteli, hogy a típusváltozót monotípussal (nem politípussal) példányosítsák.

A predikatív rendszerek közé tartozik az intuicionista típuselmélet és a Nuprl .

Impredikatív polimorfizmus

Az impredikatív (feltétel nélküli) polimorfizmus lehetővé teszi, hogy egy típusváltozót tetszőleges típussal példányosítson – mind monomorf, mind polimorf, beleértve a definiált típust is. (Ha egy számításon belül lehetővé teszi, hogy egy rendszer rekurzívan magában foglalja önmagát, azt impredikativitásnak nevezzük . Ez potenciálisan olyan paradoxonokhoz vezethet, mint Russell vagy Cantor [20] , de ez nem történik meg egy bonyolult típusú rendszer esetén [21] .)

Az impredikatív polimorfizmus lehetővé teszi, hogy polimorf függvényeket paraméterként adjon át más függvényeknek, eredményül adja vissza őket, tárolja őket adatstruktúrákban stb., ezért is nevezik első osztályú polimorfizmusnak . Ez a polimorfizmus legerősebb formája, de másrészt komoly optimalizálási problémát jelent, és feloldhatatlanná teszi a típuskövetkeztetést .

Impredikatív rendszerre példa az F rendszer és kiterjesztései (lásd lambda kocka ) [22] .

Rekurzió támogatás

Hagyományosan az ML leszármazottaiban egy függvény csak "kívülről" nézve lehet polimorf (vagyis alkalmazható különféle típusú argumentumokra), de definíciója csak monomorf rekurziót tartalmazhat (vagyis a típusfelbontás hívás előtt). Az ML típusú rekonstrukció rekurzív típusokra való kiterjesztése nem jelent komoly nehézségeket. Másrészt a típusrekonstrukció rekurzívan definiált kifejezésekkel való kombinációja egy nehéz problémát okoz, amelyet polimorf rekurziónak neveznek . Mycroft és Meertens egy polimorf tipizálási szabályt javasolt , amely lehetővé teszi, hogy a rekurzív függvények rekurzív hívásait a saját testéből különböző típusokkal példányosítsák. Ebben a Milner–Mycroft-számításként ismert számításban a típuskövetkeztetés eldönthetetlen . [23]

Strukturális típusú polimorfizmus

A terméktípusok (más néven " rekordok ") szolgálják az objektumorientált és moduláris programozás formális alapját. Kettős párjuk összegtípusokból áll ( más néven " változatok ") [24] [25] [19] :

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

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

Együtt eszközöket jelentenek bármilyen összetett adatszerkezet és a programok viselkedésének bizonyos aspektusainak kifejezésére .

A Record Calculi a probléma általános elnevezése és számos megoldása aterméktípusok programozási nyelvekben való rugalmasságára vonatkozóan a típusbiztonság feltétele mellett [26] [27] [28] . A kifejezés gyakran kiterjed az összegtípusokra, és a „ rekordtípus ” fogalmának határaikalkulusonként változhatnak (valamint maga a „ típus ” fogalma is). A " rekord polimorfizmus " (amely gyakran magában foglalja a polimorfizmus variánsait is ) [27] , a " modulusszámítás " [9] és a " strukturális polimorfizmus " kifejezéseket is használják.

Általános információk

A típustermékek és -összegek ( rekordok és változatok [ en ] rugalmasságot biztosítanak az összetett adatszerkezetek felépítésében, de sok valós típusú rendszer korlátai gyakran megakadályozzák, hogy használatuk valóban rugalmas legyen. Ezek a korlátozások általában a hatékonyság, a típuskövetkeztetés vagy egyszerűen a használhatóság miatt merülnek fel . [29]

A klasszikus példa a Standard ML , amelynek típusrendszerét szándékosan csak annyira korlátozták, hogy a könnyű kivitelezést a kifejezőkészséggel és a matematikailag igazolható típusbiztonsággal kombinálják .

Példa a rekord meghatározására :

> val r = { név = "Foo" , használt = igaz }; (* val r : {név : karakterlánc, használt : bool} = {név = "Foo", használt = igaz} *)

A mező értékéhez való hozzáférés a neve alapján az űrlap előtag-konstrukciójával történik #field record:

> val r1 = #név r ; (* val r1 : string = "Foo" *)

A következő függvénydefiníció a rekord felett helyes:

> fun name1 ( x : { név : karakterlánc , kor : int }) = #név x

És a következő fordítói hibát generál, amely szerint a típus nincs teljesen megoldva :

> fun name2 x = #name x (* feloldatlan típus a deklarációban: {name : '1, ...} *)

A rekordok monomorfizmusa rugalmatlanná, de hatásossá teszi őket [30] : mivel minden rekordmező tényleges memóriahelye előre (fordítási időben) ismert, a névre hivatkozva direkt indexelésbe fordul, amit általában egy gépben számítanak ki. utasítás. Komplex skálázható rendszerek fejlesztésekor azonban kívánatos, hogy a mezőket konkrét rekordokból absztraháljuk – például egy univerzális mezőválasztó definiálásához:

szórakoztató válasszon r l = #l r

De a különböző rekordokban eltérő sorrendben elhelyezkedő mezők polimorf hozzáférésének összeállítása nehéz probléma, mind a nyelvi szintű műveletek biztonsági ellenőrzése , mind a gépi kód szintű teljesítmény szempontjából. Naiv megoldás lehet minden hívásnál dinamikusan megkeresni a szótárt (és a szkriptnyelvek ezt használják), de ez nyilvánvalóan rendkívül nem hatékony. [31]

A típusösszegek képezik az ág kifejezés alapját , és a típusrendszer szigorúsága miatt a fordító biztosítja az elemzés teljességét. Például a következő összegtípushoz :

adattípus 'a foo = A of 'a | B of ( 'a * 'a ) | C

minden rajta lévő függvény így fog kinézni

fun bar ( p : 'a foo ) = A x = > ... | p esete B ( x , y ) => ... | c => ...

és ha bármelyik záradékot eltávolítják, a fordító figyelmeztetést ad a hiányos elemzésre (" match nonexhaustive"). Olyan esetekben, amikor a sok lehetőség közül csak néhány igényel elemzést egy adott kontextusban, lehetőség van default-elágazás megszervezésére az ún. "Joker" - univerzális minta, amellyel az összes érvényes (a gépelés szerint) érték összehasonlítható. Aláhúzással (" ") van írva _. Például:

fun bar ( p : 'a foo ) = C = > ... | p esete _ => ...

Egyes nyelvekben (a szabványos ML -ben, a Haskellben ) még az "egyszerűbb" konstrukció if-then-elseis csak szintaktikai cukor az elágazás egy speciális esete , azaz a kifejezés

ha A , akkor B más C

már a nyelvtani elemzés szakaszában formában kerül bemutatásra

igaz A eset = > B | hamis => C

vagy

igaz A eset = > B | _ => C

Szintaktikus cukor

A Standard ML -ben a rekordok és változatok monomorfok, azonban a több mezőt tartalmazó rekordok kezelésére szolgáló szintaktikai cukor támogatott, az úgynevezett " univerzális minta " [32] :

> val r = { név = "Foo" , használt = igaz }; (* val r : {név : karakterlánc, használt : bool} = {név = "Foo", használt = igaz} *) > val { használt = u , ...} = r ; (* érték u : bool = igaz *)

A „ {used, ...}” típusú ellipszis azt jelenti, hogy az említetteken kívül más mezők is léteznek ebben a rekordban. Azonban nincs rekord polimorfizmus mint olyan (még a prenex sem ): a monomorf rekordtípus információinak teljes statikus felbontása ( következtetéssel vagy explicit annotációval ) szükséges.

Rekordok bővítése és funkcionális frissítése

A bővíthető rekordok kifejezést olyan műveletek általános megjelölésére használják, mint a bővítés (új rekord készítése egy meglévő rekord alapján új mezők hozzáadásával), a kivágás (meglévő rekordból egy meghatározott rész eltávolítása) stb. magában foglalja az úgynevezett „funkcionális rekordfrissítés” (functional record update) lehetőségét - a meglévő rekord alapján új rekordérték létrehozásának műveletét a mezői nevének és típusának másolásával, amelyben egy vagy több mező az új rekord új értékeket kap, amelyek eltérnek az eredetitől (és esetleg más típusúak is). [33] [34] [19] [35] [36] [37]

Önmagukban a funkcionális frissítési és bővítési műveletek ortogonálisak a polimorfizmus rögzítésére, de polimorf használatuk különösen érdekes. Még a monomorf rekordok esetében is fontossá válik, hogy el lehessen hagyni a változatlanul másolt mezők kifejezett említését, és ez tulajdonképpen rekord polimorfizmust jelent tisztán szintaktikai formában . Másrészt, ha a rendszerben lévő összes rekordot bővíthetőnek tekintjük, akkor ez lehetővé teszi, hogy a rekordokon lévő függvények polimorfként legyenek tipizálva.

A legegyszerűbb tervezési változat egy példája az Alice ML -ben valósul meg (a jelenlegi utód ML konvenciók szerint ) [36] . Az univerzális minta (ellipszis ) kibővített lehetőségekkel rendelkezik: „sor rögzítésére” használható, hogy a rekord „megmaradó” részét értékként kezelje:

> val r = { a = 1 , b = igaz , c = "helló" } (* r = {a = 1, b = igaz, c = "helló"} *) > val { a = n , ... = r1 } = r (* r1 = {b=igaz, c="helló"} *) > val r2 = { d = 3,14 , ... = r1 } (* r2 = {b=igaz, c="helló ", d=3,14} *)

A funkcionális frissítés egy sor szolgáltatásszóval történő rögzítésének származékakéntwhere valósul meg . Például a következő kód:

> legyen val r = { a = 1 , c = 3.0 , d = "nem lista" , f = [ 1 ], p = [ "nem karakterlánc" ], z = NINCS } in { r ahol d = nil , p = "helló" } vége

automatikusan átíródik a következő formában:

> legyen val r = { a = 1 , c = 3.0 , d = "nem lista" , f = [ 1 ], p = [ "nem karakterlánc" ], z = NINCS } val { d = _, p = _, ... = tmp } = r in { ... = tmp , d = null , p = "helló" } vége

Rekordösszefűzés

Az egyik első ( 1980 -as évek vége – 1990-es évek eleje ) különféle lehetőségeket javasolt a bővíthető rekordok formalizálására a nem polimorf rekordokon végzett összefűzési műveletekkel (Harper-Pearce [38] , Wand [39] , Salzmann [40] ). Cardelli még rekordműveleteket is használt a polimorfizmus helyett az Amber nyelvben. Nincs ismert módszer ezeknek a kalkulusoknak a hatékony összeállítására; ráadásul ezek a számítások a típuselméleti elemzés szempontjából igen összetettek . [27] [41] [42] [43]

Például [33] :

val car = { név = "Toyota" ; kor = "régi" ; id = 6678 } val truck = { name = "Toyota" ; id = 19823235 } ... val repaired_truck = { autó és teherautó }

sorpolimorfizmus szerzője ) megmutatta, hogy rekordösszefűzéssel modellezhető a többszörös öröklődés [39] [33] .

Strukturális altípusok: Cardelli

Luca Cardelli feltárta a „ rekordpolimorfizmus ” formalizálásának lehetőségét a rekordok altípus-kapcsolatai révén : ehhez a rekordot „univerzális altípusként” kezelik, azaz értéke a szupertípusainak teljes halmazára vonatkozhat. Ez a megközelítés támogatja a metódusok öröklését is , és típuselméleti alapként szolgál az objektum-orientált programozás leggyakoribb formáihoz. [27] [44] [45]

Cardelli egy variációt mutatott be a rekord polimorfizmus összeállításának módszerére az altípusaik között oly módon, hogy előre meghatározta az összes lehetséges címke eltolását egy potenciálisan hatalmas struktúrában, sok üres hellyel [31] .

A módszernek jelentős hátrányai vannak. Az altípusozás támogatása a típusrendszerben nagymértékben bonyolítja a típuskonzisztencia -ellenőrző mechanizmust [46] . Ezen túlmenően, jelenlétében a kifejezés statikus típusa már nem ad teljes információt a bejegyzés értékének dinamikus szerkezetéről . Például, ha csak altípusokat használ, a következő kifejezés:

> ha igaz , akkor { A = 1 , B = igaz } else { B = hamis , C = "Cat" } (* val it : {B : bool} *)

típussal rendelkezik {B : bool}, de dinamikus értéke egyenlő a -val {A = 1, B = true}, vagyis a kibővített rekord típusára vonatkozó információ elveszik [43] , ami komoly problémát jelent olyan műveletek ellenőrzésénél , amelyek végrehajtásához teljes körű információra van szükség az értékstruktúráról (pl. az egyenlőség összehasonlítása ) [19] . Végül altípusok jelenlétében a rekordok rendezett és rendezetlen ábrázolása közötti választás komolyan befolyásolja a teljesítményt [47] .

Az altípusok népszerűsége annak köszönhető, hogy számos problémára ad egyszerű és vizuális megoldást. Például a különböző típusú objektumok egyetlen listába helyezhetők, ha van egy közös szupertípusuk [48] .

Wanda sor polimorfizmus

Mitchell Wand 1987 - ben javasolta a(nem kifejezetten meghatározott) részével kapcsolatos információk rögzítését az általa sortípusú változón keresztül ( sor típusú változó ) [49] .

A sorváltozó olyan típusú változó, amely beírt mezők véges halmazain (sorain) fut (" (значение : тип)" párjain). Az eredmény az a képesség, hogy az ML -t alátámasztó parametrikus polimorfizmuson túl széles körű öröklődést valósítson meg anélkül, hogy a típusrendszert altípusozási szabályokkal bonyolítaná A kapott polimorfizmust sorpolimorfizmusnak nevezzük . Az inline polimorfizmus kiterjed a típusok szorzatára és a típusösszegekre is .

Vand a kifejezést az angoloktól kölcsönözte . sor (sor, lánc, sor) az Algol-68- ból , ahol nézethalmazt jelentett. Az orosz nyelvű irodalomban ezt a kifejezést az Algol kontextusában hagyományosan "többfajúnak" fordították. Létezik a "sorváltozók" kifejezés "karakterláncváltozóként" való fordítása is [41] , ami összetévesztést okozhat a karakterlánctípusok kisbetűivel .

Példa ( OCaml nyelv ; postfix szintaxis, record#field) [50] :

# legyen send_m a = a # m ;; (* érték send_m : < m : a; .. > -> a = <fun> *)

Itt a (két pontból álló) ellipszis az OCaml által elfogadott szintaxis egy névtelen soron belüli típusú változóhoz . Az ilyen beírás miatt a függvény bármely (korábban nem ismertsend_m ) objektumtípusra alkalmazható , amely tartalmazza a megfelelő aláírás metódusát. m

A Wanda kalkulus típuslevonása az eredeti verzióban hiányos volt: a sorozat bővítésére vonatkozó korlátozások hiánya miatt a mező hozzáadása, ha a név egyezik, felváltja a meglévőt - ennek eredményeként nem minden programnak van fő típusa [6] [43] . Ez a rendszer volt azonban az első konkrét javaslat az ML kiterjesztésére az öröklődést támogató rekordokkal [51] . A következő években számos különböző fejlesztést javasoltak, beleértve azokat is, amelyek teljessé teszik [51] [27] .

A legfigyelemreméltóbb nyomot Didier Remy ( franciául Didier Rémy ) hagyta. Gyakorlatias típusrendszert épített ki bővíthető rekordokkal, beleértve egy teljes és hatékony típusrekonstrukciós algoritmust [52] [53] . Remy a típusok nyelvét fajtákba rétegzi, és a típusok rendezett algebráját fogalmazza meg ( eng. sorted algebra of type, sorted language of type ). Különbséget teszünk a tulajdonképpeni típusok (beleértve a mezőtípusokat is) és a mezők fajtája között ; bevezetik a köztük lévő leképezéseket és ezek alapján megfogalmazzák a kiterjesztett rekordok gépelésének szabályait a klasszikus ML szabályok egyszerű kiterjesztéseként . A mező jelenléti információi a típusrendezés és a mezőrendezés közötti leképezésként vannak definiálva . A sor típusú változók a mezőrendezéshez tartozó változókként vannak újrafogalmazva, és egyenlők a hiány állandóval , amely a mezőrendezés olyan eleme, amely nem egyezik a típusrendezésben . Egy n mezőből álló rekord típuskiértékelési művelete egy n-es mező leképezése egy típusra (ahol a tuple minden mezőjét vagy a jelenléti függvény számítja ki, vagy a távolléti konstans adja meg ).

Leegyszerűsítve a kalkulus gondolata úgy értelmezhető, mint a rekord bármely mezőjének típusának kiterjesztése egy jelenlét/hiányzásjelzővel , és a rekordot egy sorként ábrázolja minden lehetséges mezőhöz [6] . Az implementációs prototípusban a típusnyelv szintaxisa közelebb került a típuselméleti megfogalmazáshoz, például [52] :

# let car = { name = "Toyota" ; kor = "régi" ; id = 7866 } ;; (* autó : ∏ (név: elő (karakterlánc); azonosító: pre (szám); életkor: pre (karakterlánc); abs) *) # let truck = { name = "Blézer" ; id = 6587867567 } ;; (* teherautó : ∏ (név : pre (string); id : pre (szám); abs) *) # let person = { name = "Tim" ; életkor = 31 ; id = 5656787 } ;; (* személy : ∏ (név: elő (karakterlánc); azonosító: pre (szám); életkor: pre (szám); abs) *)

(a szimbólum ∏a Remyben a típusszámítási műveletet jelenti)

Egy új mező hozzáadása a következő konstrukcióval írható with:

# engedje meg a vezetőt = { járművel rendelkező személy = autó } ;; (* sofőr : ∏ (jármű : pre (∏ (név : elő (karakterlánc); azonosító: pre (szám); életkor: pre (karakterlánc); abs)); név: pre (karakterlánc); azonosító: pre (szám) ; életkor : elő (szám); abs) *)

A funkcionális frissítés ugyanúgy meg van írva, azzal a különbséggel, hogy egy már létező mező említése felülírja:

# let truck_driver = { sofőr járművel = teherautó } ;; (* teherautó-sofőr : ∏ (jármű : pre (∏ (név : pre (karakterlánc); id : pre (szám); abs)); név : pre (karakterlánc); id : pre (szám); életkor: elő (szám) ); abs) *)

Ez a séma formalizálja az iratokon végzett műveletek ellenőrzéséhez és a fő típus kikövetkeztetéséhez szükséges kényszert , de nem vezet nyilvánvaló és hatékony megvalósításhoz [6] [43] . A Remy hash-t használ, ami átlagosan meglehetősen hatékony, de megnöveli a futási időt még a natívan monomorf programok esetében is, és kevéssé alkalmas sok mezőt tartalmazó rekordokhoz [31] .

Rémy tovább vizsgálta a soron belüli polimorfizmus használatát az adataltípusozással összefüggésben , hangsúlyozva, hogy ezek ortogonális fogalmak, és megmutatta, hogy a rekordok akkor válnak a legkifejezőbbé, ha együtt használják [54] . Ennek alapján Jérôme Vouillonnal közösen javasolta az ML könnyű objektumorientált kiterjesztését [55] . Ezt a bővítményt Xavier Leroy „Caml Special Light” nyelvén valósították meg, OCaml -lé alakítva [56] . Az OCaml objektummodell szorosan összefonódik a strukturális altípusok használatával és az inline polimorfizmussal [48] , ezért néha tévesen azonosítják őket. Az OCaml inline termékpolimorfizmusa a típuskövetkeztetés középpontjában áll ; Az altípus-kapcsolatok nem szükségesek egy támogatott nyelven, de tovább növelik a rugalmasságot a gyakorlatban [55] [50] [48] . Az OCaml egyszerűbb és leíróbb szintaxissal rendelkezik a típusinformációkhoz.

Jacques Garrigue ( fr. Jacques Garrigue ) megvalósította [25] a polimorf összegek gyakorlati rendszerét . Remi és Ohori elméleti munkásságát ötvözte , egy középen futó rendszert épített fel: a címkék rekordban való jelenlétére vonatkozó információkat nemek segítségével ábrázolják, a típusaikra vonatkozó információk pedig soron belüli változókat használnak. Annak érdekében, hogy a fordító különbséget tegyen a polimorf és a monomorf összegek között, Garriga speciális szintaxist (backtick, prefix tag) használ. Ez kiküszöböli a típusdeklaráció szükségességét – azonnal írhatunk rá függvényeket, és a fordító a címkék minimális listáját adja ki a függvények összeállítása közben. Ez a rendszer 2000 körül vált az OCaml részévé , de nem a helyett , hanem a monomorf összegek mellett, mivel ezek valamivel kevésbé hatékonyak, és mivel nem tudják ellenőrizni az elemzés teljességét , megnehezítik a hibák megtalálását (ellentétben a Bloom-féle rendszerrel megoldás ). [25] [57]

A Wand-féle inline polimorfizmus hátránya az implementáció nem nyilvánvalósága (nincs egységes szisztematikus módja annak összeállítására, minden konkrét, soron belüli változókon alapuló típusrendszernek megvan a maga implementációja), valamint az elmélettel való kétértelmű kapcsolat (nincs egységes a típusellenőrzés és a következtetés megfogalmazása , a következtetés támogatása külön megoldott és kísérleteket igényelt különféle korlátozások kiszabásával) [27] .

Átlátszó Harper-Lilybridge összegek

A legösszetettebb típusú rekordok a függő rekordok. Az ilyen rekordok típusokat és "közönséges" értékeket is tartalmazhatnak (materializált típusok, reified [9] ), és az irattörzsben a sorrendben következő kifejezések és típusok az őket megelőzők alapján határozhatók meg. . Az ilyen jelölések megfelelnek a függő típuselmélet „ gyenge összegeinek ” , más néven „ egzisztenciálisoknak ”, és a programnyelvi modulrendszerek legáltalánosabb indoklásaként szolgálnak [58] [59] . Cardelli [60] hasonló tulajdonságú típust tekintett a teljes típusú programozás egyik fő típusának (de " rekordoknak " nevezte őket).

Robert Harper és Mark Lillibridge megkonstruálta [61 ] [59] az áttetsző összegszámítást , hogyformálisan igazolja a magasabb rendű első osztályú modulnyelvet , a legfejlettebb ismert modulrendszert . Ezt a számítást többek között a Harper-Stone szemantikában használják , amely a Standard ML típuselméleti igazolását jelenti.

Az áttetsző összegek általánosítanak gyenge összegeket címkéken és a típuskonstruktorokat leíró egyenlőségek halmazán keresztül . Az áttetsző kifejezés azt jelenti , hogy egy rekordtípus tartalmazhat mindkét típust kifejezetten exportált szerkezettel, valamint teljesen absztraktakat is . A kalkulusban a nemzetségek rétege egyszerű klasszikus összetételű: minden típus neme és funkcionális nemzetségei megkülönböztetve vannak , tipizálnak típusú konstruktorokat ( az ML nem támogatja a polimorfizmust magasabb nemzetségekben , minden típusváltozó a nemzetséghez tartozik , és a típuskonstruktorok absztrakciója csak funktorokon keresztül lehetséges [62 ] ). A kalkulus az "altípusok" és "almezők" figyelembevételével megkülönbözteti az altípusok szabályait a rekordokra , mint alaptípusokra és a rekordmezőkre, mint azok összetevőire, míg a mezőaláírások kitakarása (absztrakciója) külön fogalom az altípusozástól. Az altípus itt formalizálja a modulok interfészekhez való hozzárendelését . [61] [9] $\star$ ${\displaystyle k_{1}=>k_{2))$ $\star$

A Harper-Lilybridge kalkulus még a típuskonzisztencia -ellenőrzés szempontjából is eldönthetetlen ( a szabványos ML -ben és OCaml - ben megvalósított modulnyelvi dialektusok ennek a kalkulusnak korlátozott részhalmazait használják). Később azonban Andreas Rossberg az ő ötleteik alapján megépítette az „ 1ML ” nyelvet, amelyben a nyelv hagyományos magszintű rekordjai és a modulszintű struktúrák ugyanazok az első osztályú konstrukciók [9] (szignifikánsan kifejezőbbek, mint Cardelli-féle – lásd az ML modulnyelv kritikáját ). Harper és Mitchell [63] beépítésével, miszerint minden típust fel kell osztani „kis” és „nagy” típusú univerzumokra (leegyszerűsítve ez hasonlít a típusok egyszerű és összesített típusokra való alapvető felosztásához, egyenlőtlen gépelési szabályok), a Rossberg nem csak a konzisztencia ellenőrzését , hanem a szinte teljes típuskövetkeztetést is biztosította a feloldhatóságnak . Ráadásul az 1ML lehetővé teszi az impredikatív polimorfizmust [64] . Ugyanakkor a belső nyelv 1ML-ben az F ω lapos rendszeren alapul, és nem igényli a függő típusok metaelméletként való használatát. 2015 -től Rossberg nyitva hagyta annak lehetőségét, hogy inline polimorfizmust adjon az 1ML -hez , megjegyezve, hogy ennek teljesebb típuskövetkeztetést kell biztosítania [ 9] . Egy évvel később hozzáadta [65] az effektusok polimorfizmusát az 1ML-hez .

Ohori rekordok polimorf kalkulusa

Atsushi Ohori felügyelőjével , Peter Bunemannal együtt 1988-ban javasolta azt az ötletet , hogy korlátozzák a közönséges típusú változók lehetséges értékeinek tartományát maguknak a rekordoknak a polimorf tipizálásában . Később Ohori ezt az elképzelést a jelölési nemzetségeken keresztül formalizálta , miután 1995-re felépített egy teljes értékű kalkulust és egy módszert annak hatékony összeállítására [19] [30] . Az implementációs prototípust 1992 -ben hozták létre az SML/NJ [66] fordító kiterjesztéseként, majd Ohori vezette saját SML# fordítóját, amely az azonos nevű Standard ML dialektust valósítja meg . Az SML# -ban a rekordpolimorfizmus szolgál alapul az SQL - konstrukciók SML - programokba való zökkenőmentes beágyazásához . Az SML# -t a nagy japán vállalatok használják a nagy terhelésű adatbázisokkal kapcsolatos üzleti problémák megoldására [67] . Példa egy ilyen munkamenetre ( REPL ) [68] :

szórakoztató gazdag { Fizetés = s , ... } = s > 100000 ; (* val wealthy = fn : 'a#{ Fizetés:int, ... } -> bool *) vidám fiatal x = #Kor x < 24 ; (* val young = fn : 'a#{ Age:int, ... } -> bool *) fun youngAndWealthy x = gazdag x és fiatal x is ; (* val youngAndWealthy = fn : 'a#{ Kor:int, Fizetés:int, ... } -> bool *) fun select display l pred = fold ( fn ( x , y ) => if pred x then ( display x ) ::y else y ) l nil ; (* val select = fn : ('a -> 'b) -> 'a lista -> ('a -> bool) -> 'b lista *) fun youngAndWealthyEmployees l = select #Name l youngAndWealthy ; (* val youngAndWealthyEmployees = fn : 'b#{ Életkor:int, Név:'a, Fizetés:int, ... } lista -> 'a lista *)

Ohori „rekordpolimorfizmusnak ” ( angol rekord polimorfizmus ) vagy „ polimorf rekordszámításnak ” ( angol polymorphic record calculus ) nevezte kalkulusát, egyúttal hangsúlyozva, hogy Wandhoz hasonlóan ő is nemcsak terméktípusok, hanem típusok polimorfizmusát is figyelembe veszi . összegek [27] .

Az Ohori-kalkulust a nemzetségréteg legintenzívebb felhasználása jellemzi [6] . A bejegyzésben (hivatkozás típusa nemzetségre ) a szimbólum vagy az összes típus nemzetségét jelenti ; vagy a rekord nemzetség , amelynek alakja , jelöli az összes rekord halmazát, amely legalább a megadott mezőket tartalmazza; vagy egy variáns nemzetség , amelynek alakja az összes változattípus halmazát jelöli, amely legalább a megadott konstruktorokat tartalmazza . A nyelv lapos szintaxisában valamilyen jelölés típusmegszorítása így van írva (lásd a fenti példákat). A megoldás némileg hasonló Cardelli-Wegner [27] korlátozott kvantifikációjához ] . $t\colon \colon k$ $t$ $k$ $k$ $U$ ${\displaystyle \left\{\left\{l_{1}\colon t_{1},\dots ,l_{n}\colon t_{n}\right\}\right\))$ $\left\langle \left\langle l_{1}:t_{1},\dots ,l_{n}\colon t_{n}\right\rangle \right\rangle$ t#{...}

Az egyetlen polimorf művelet, amelyet ez a kalkulus biztosít, a mező extrakciós művelet [69] . Azonban Ohori volt az első, aki bevezetett egy egyszerű és hatékony összeállítási sémát rekordpolimorfizmushoz [43] . Ezt a "megvalósítások kalkulusának" ( végrehajtási kalkulusnak ) nevezte. A rekordot az eredeti rekord mezőnevei szerint lexikográfiailag rendezett vektor ábrázolja ; egy mező név szerinti megcímzése egy közbülső függvény hívását jelenti, amely az adott vektorban az adott mező számát adja vissza a kért névvel, majd ezt követően a vektort indexeli a számított pozíciószámmal. A függvényt csak polimorf kifejezések példányosításakor hívják meg, ami minimális többletköltséget ró a futási időre polimorfizmus használatakor, és nem ír elő többletköltséget, ha monomorf típusokkal dolgozik. A módszer tetszőlegesen nagy bejegyzésekkel és változatokkal egyaránt jól működik. A kalkulus típuskövetkeztetést biztosít , és erős egyezést talál az elmélettel (az általános kvantifikáció közvetlenül kapcsolódik a szokásos vektorindexeléshez ), mivel a Girard-Reynolds másodrendű lambda-számítás közvetlen kiterjesztése , amely lehetővé teszi a polimorf különböző jól ismert tulajdonságait. a tipizálást át kell vinni rekord polimorfizmusba [31] .

A gyakorlatban a polimorf változatok támogatása SML# -ban nem valósult meg, mivel az nem kompatibilis a Standard ML összegtípus - definíciós mechanizmusával (az összegek és a rekurzív típusok szintaktikai elválasztását igényli) [70] .

Az Ohori-számítás hátránya a rekordbővítési vagy -csonkítási műveletek támogatásának hiánya [27] [71] [43] .

Első osztályú Guster-Jones jegyek

A minősített típusok elméletében a bővíthető rekordokat egy mező hiányával ( "hiányzik" predikátum ) és egy mező ( "has" predikátum ) predikátum jelenlétével írják le. Benedict Gaster ( Benedict R. Gaster ) az elmélet szerzőjével, Mark Jones-szal ( Mark P. Jones ) együtt véglegesítette azt a bővíthető rekordok tekintetében implicit módon tipizált nyelvek gyakorlati típusrendszerére, beleértve a fordítási módszer meghatározását is [6] . Az első osztályú címkék kifejezést a statikusan ismert címkékből a mezőműveletek elvonatkoztatásának képessége hangsúlyozzák . Később Gaster megvédte értekezését [72] a felépített rendszerről .

A Gaster-Jones kalkulus nem ad teljes típusú következtetést . Ezen túlmenően az eldönthetőségi problémák miatt mesterséges korlátozást is bevezettek: az üres sorozatok tilalmát [73] . Sulzmann megpróbálta újrafogalmazni a kalkulust [40] , de az általa felépített rendszer nem terjeszthető ki a polimorf rekordbővítés támogatására, és nem rendelkezik univerzális hatékony fordítási módszerrel [43] .

Daan Leijen hozzáadott egy soregyenlőségi predikátumot (vagy soregyenlőségi predikátumot ) a Gaster-Jones-számításhoz , és a sorozatok nyelvét áthelyezte a predikátumok nyelvére - ez biztosította a teljes típuskövetkeztetést , és feloldotta az üres sorozatok tilalmát [74] . Összeállításkor a rekordokat lexikográfiailag rendezett sorrá alakítják át, és a bizonyíték fordítást alkalmazzák a Gaster-Jones séma szerint. A Layen rendszere lehetővé teszi olyan kifejezések kifejezését , mint a magasabb rendű üzenetek (az objektum-orientált programozás legerősebb formája ) és az első osztályú ágak .

Ezen munkák alapján a Haskell nyelv [75] kiterjesztései valósultak meg .

Gaster-Jones eredményei nagyon közel állnak Ohori eredményeihez, a típuselméleti indokolásban mutatkozó jelentős eltérések ellenére , és a fő előny a rekordbővítési és -csonkítási műveletek támogatása [6] . A kalkulus hátránya, hogy a típusrendszer olyan tulajdonságaira támaszkodik, amelyek a legtöbb programozási nyelvben nem találhatók meg. Emellett a típuskövetkeztetés is komoly problémát jelent, ezért a szerzők további megszorításokat vezettek be. És bár a Layen sok hiányosságot kiküszöbölt, a -branch használata nem lehetséges. [71]default

Kontrollkonstrukció polimorfizmus

A szoftverrendszerek fejlődésével az összeg típusú opciók száma növekedhet , és az egyes opciók hozzáadásához minden függvényhez hozzá kell adni egy megfelelő ágat ezen a típuson keresztül, még akkor is, ha ezek az ágak a különböző függvényekben azonosak. Így a legtöbb programozási nyelvben a funkcionalitás növelésének összetettsége nem lineárisan függ a feladatmeghatározás deklaratív változásaitól. Ez a minta kifejezési problémaként ismert . Egy másik jól ismert probléma a kivételkezelés : a típusrendszerekkel kapcsolatos több évtizedes kutatások során minden típusbiztosnak minősített nyelv még mindig ki tudott lépni egy meg nem fogott kivételt dobva – ugyanis maguk a kivételek tipizálása ellenére a felvetés mechanizmusa és kezelésük nem volt gépelve. Míg a kivételek áramlásának elemzésére szolgáló eszközöket építettek, ezek az eszközök mindig is a nyelven kívüliek voltak.

Matthias Blume , Andrew Appel munkatársa , aki a projekt utódján, ML [76] dolgozott , végzős hallgatója, Wonseok Chae és kollégája, Umut Acar mindkét problémát matematikai dualitás szorzatok és összegek alapján oldotta meg . Elképzeléseik megtestesítője az MLPolyR [71] [34] [77] nyelv volt, amely a Standard ML legegyszerűbb részhalmazán alapult, és kiegészítette azt a típusbiztonság több szintjével [78] . Wonseok Chai később ezekről az eredményekről védte meg disszertációját [78] .

A megoldás a következő. A dualitás elve szerint egy fogalom bevezető alakja megfelel a duális eliminációs formájának [ 71] . Így az összegek eliminációs formája (ágak elemzése) megfelel a bejegyzések bevezető formájának. Ez arra ösztönzi az elágazást, hogy ugyanazokkal a tulajdonságokkal rendelkezzen, amelyek már elérhetők a bejegyzéseknél – tegye első osztályú objektumokat , és lehetővé tegye a kiterjesztést.

Például a legegyszerűbb kifejezési nyelvi tolmács:

fun eval e = eset e of `Const i => i | `Plusz (e1,e2) => eval e1 + eval e2

az első osztályú konstrukció bevezetésével casesátírható a következőre:

fun eval e = egyezik az e -vel az esetekkel `Const i => i | `Plusz (e1,e2) => eval e1 + eval e2

ami után casesa -blokk renderelhető:

fun eval_c eval = esetek `Const i => i | `Plusz (e1,e2) => eval e1 + eval e2 fun eval e = egyezik e -vel (eval_c eval)

Ez a megoldás lehetővé teszi defaultaz -elágazást (ellentétben a Gaster-Jones kalkulussal ), ami az első osztályú ágak összetétele szempontjából fontos [34] . A sor kompozíciójának kiegészítése a szó segítségével történik . nocases

fun const_c d = esetek `Const i => i alapértelmezett : d fun plus_c eval d = esetek `Plus (e1,e2) => eval e1 + eval e2 alapértelmezett : d fun eval e = egyezik az e -vel a const_c-vel (plus_c eval nocases ) fun bind env v1 x v2 = ha v1 = v2 , akkor x else env v2 fun var_c env d = esetek `Var v => env v alapértelmezett : d fun let_c eval env d = esetek `Let (v,e,b) => eval (bind env v (eval env e)) b alapértelmezett : d fun eval_var env e = egyezik az e -vel const_c-vel (plus_c (eval_var env) (var_c env (let_c eval_var env nocases )))

Mint látható, az új kód, amelyet a rendszer minőségi bonyolultságával kell hozzáadni, nem igényli a már megírt kód megváltoztatását (a függvények const_cés a plus_c"semmit sem tud" a változók és let-blokkok támogatásának későbbi kiegészítéséről a nyelvi tolmács). Így az első osztályú bővíthető esetek alapvető megoldást jelentenek az kifejezési problémára , lehetővé téve, hogy egy kiterjeszthető programozási paradigmáról beszéljünk [71] [78] . inline polimorfizmus használatára , amely már a típusrendszerben is támogatott, és ebben az értelemben egy ilyen műszaki megoldás előnye a fogalmi egyszerűsége [ 34] .

A szoftverrendszerek kiterjesztése azonban megköveteli a kivételek kezelésének ellenőrzését is , amelyek tetszőleges hívásbeágyazási mélységben dobhatók fel. És itt Bloom és munkatársai egy új típusú biztonsági szlogent hirdetnek Milner szlogenjének kidolgozásában : " A típusellenőrzésen átmenő programok nem okoznak kezeletlen kivételeket ." A probléma az, hogy ha a függvénytípus -aláírás információkat tartalmaz azokról a kivételekről, amelyeket ez a függvény potenciálisan dobhat, és ennek az információnak az átadott függvény aláírásában szigorúan konzisztensnek kell lennie a magasabb rendű függvényparaméter információival (beleértve, ha ez egy üres halmaz ) - a kivételkezelési mechanizmus beírása azonnal megköveteli magának a kivételek típusainak polimorfizmusát - ellenkező esetben a magasabb rendű függvények megszűnnek polimorfak lenni. Ugyanakkor biztonságos nyelven a kivételek egy kiterjeszthető összeg [79] [80] [81] , vagyis egy olyan változattípus, amelynek a konstruktorai a program előrehaladtával adódnak hozzá. Ennek megfelelően a kivételes áramlási típusú biztonság azt jelenti, hogy támogatni kell a nyújtható és polimorf összegtípusokat is . A megoldás itt is az inline polimorfizmus .

Akárcsak a Garriga kalkulus , az MLPolyR is speciális szintaxist használ a polimorf összegekhez (backtick, vezető tag), és nincs szükség az összeg típusának előzetes deklarálására (vagyis a fenti kód a teljes program, nem töredék). Előnye, hogy nincs probléma az elemzés teljesség-ellenőrzésével: az MLPolyR szemantikáját egy bizonyított megbízhatóságú belső nyelvre való konvertálással határozzuk meg , amely nem támogatja sem az összegzési polimorfizmust, sem a kivételeket (nem is beszélve a nem megragadott kivételekről), így ezekre szükség van. A fordítási idejű törlés maga is a megbízhatóság bizonyítéka. [34]

Az MLPolyR több kalkulus és kétlépcsős fordítás nem triviális kombinációját használja. A Remy kalkulust használja a típuslevonáshoz és a típusillesztéshez , miközben a matematikai kettősség elvét használja az összegek való megjelenítésére, majd a nyelvet egy köztes, kifejezetten tipizált nyelvre fordítja polimorf rekordokkal, majd Ohori hatékony fordítási módszerét használja. . Más szavakkal, Ohori kompilációs modelljét általánosították, hogy támogassa a Remy-számítást [69] . Típuselméleti szinten Bloom egyszerre több új szintaktikai jelölést vezet be, lehetővé téve a kivételek és az első osztályú elágazások beírásának szabályait. Az MLPolyR típusú rendszer teljes típuskövetkeztetést biztosít , így a szerzők felhagytak a típusok explicit írására szolgáló lapos szintaxis és az aláírások modulnyelven történő támogatásával .

A Leyen típusú rendszer az ág polimorfizmus egy változatát is bevezeti: egy konstrukció ábrázolható magasabb rendű függvényként , amely olyan függvényekből kap bejegyzést , amelyek mindegyike egy adott számítási ágnak felel meg ( a Haskell -féle szintaxis megfelelő ehhez a változáshoz, és nem igényel felülvizsgálatot). Például: case

dataList a = nil :: { } | hátrányok :: { hd :: a , tl :: List a } snoc xs r = eset ( fordított xs ) r utolsó xs = snoc xs { nil = \ r -> _ | _ , cons = \ r -> r . hd }

Mivel a Layen rendszerében a rekordok bővíthetők, az ágelemzés rugalmas a dinamikus döntések szintjén (például láncellenőrzések vagy asszociatív tömb használata ), de sokkal hatékonyabb megvalósítást biztosít (a változatcímke a rekordban lévő eltolásnak felel meg). Ebben az esetben azonban az alapértelmezett elágazási támogatást ( default) el kell hagyni, mivel egyetlen default-minta több mezővel (és így többszörös eltolásokkal) egyezne. Leyen ezt a konstrukciót " első osztályú mintáknak " ( első osztályú mintáknak ) nevezi.

Polimorfizmus magasabb nemeknél

A magasabb típusú polimorfizmus absztrakciót jelent a magasabb rendű típusú konstruktorok , azaz az űrlap felett

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

Ennek a funkciónak a támogatása magasabb szintre emeli a polimorfizmust, absztrakciót biztosítva mind a típusok, mind a típuskonstruktorok felett , ahogy a magasabb rendű függvények az értékek és más függvények absztrakcióját is. A magasabb nemek polimorfizmusa számos funkcionális programozási idióma természetes összetevője , beleértve a monádokat , a hajtogatásokat és a beágyazható nyelveket . [62] [82]

Például [62] , ha a következő függvényt határozza meg ( Haskell nyelv ):

amikor b m = ha b , akkor m egyébként visszatér ()

akkor a következő funkcionális típus lesz levezetve rá :

mikor :: forall ( m :: * -> * ) . Monád m => Bool -> m () -> m ()

Az aláírás m :: * -> *azt mondja, hogy a típusváltozó m egy magasabb fajtához tartozó típusváltozó ( angolul high- kinded type variable ). Ez azt jelenti, hogy elvonatkoztat a típuskonstruktorok (jelen esetben az unary , például Maybevagy []), amelyek konkrét típusokra, például Intvagy (), új típusok létrehozására alkalmazhatók.

Azokban a nyelvekben, amelyek támogatják a teljes típusú absztrakciót ( Standard ML , OCaml ), minden típusváltozónak egy nemzetséghez kell tartoznia *, különben a típusrendszer nem lenne biztonságos . A magasabb nemzetségekben a polimorfizmust tehát maga az absztrakciós mechanizmus biztosítja, a példányosításkor explicit annotációval kombinálva, ami némileg kényelmetlen. Azonban a polimorfizmus idiomatikus megvalósítása magasabb nemzetségekben is lehetséges anélkül, hogy kifejezett annotációt igényelne - ehhez a defunkcionalizáláshoz hasonló technikát alkalmaznak típus szinten . [62]

Általános polimorfizmus

A kedves rendszerek maguknak a típusrendszereknek a biztonságát biztosítják azáltal,hogy lehetővé teszik a típuskifejezések jelentésének szabályozását .

Például legyen kötelező a szokásos " vektor " típus (lineáris tömb) helyett a "hosszúságvektor" típuscsalád implementálása, vagyis a " hosszan nindexelt vektor " típus meghatározása . A klasszikus Haskell implementáció így néz ki [83] :

adat Nulla adat Succ n adat Vec :: * -> * -> * ahol Nil :: Vec a Zero Cons :: a -> Vec a n -> Vec a ( Succ n )

Itt először a fantomtípusokat [84] határozzuk meg , vagyis azokat, amelyek nem rendelkeznek dinamikus reprezentációval. A kivitelezők Zero és Succa "típusréteg értékként" szolgálnak, a változó npedig a kivitelező által megszerkesztett különböző betontípusok egyenlőtlenségét kényszeríti ki Succ. A típus általánosított algebrai adattípusként (GADT) Vecvan definiálva .

A megoldás feltételesen feltételezi, hogy a fantomtípussal a Peano-axiómák alapján nmodellezzük a vektor integer paraméterét – azaz csak olyan kifejezések épülnek fel, mint például , stb . , ők maguk is típusolatlan módon vannak megfogalmazva. Ez látható az aláírásból , ami azt jelenti, hogy a paraméterként átadott betontípusok a nemzetségbe tartoznak , ami azt jelenti, hogy bármilyen konkrét típus lehet. Más szóval, az olyan értelmetlen típusú kifejezések, mint vagy nem tiltottak itt . [83]Succ ZeroSucc Succ ZeroSucc Succ Succ ZeroVec :: * -> * -> * *Succ BoolVec Zero Int

Egy fejlettebb számítás lehetővé teszi a típusparaméter tartományának pontosabb megadását:

adatok Nat = nulla | Succ Nat adatok Vec :: * -> Nat -> * ahol VNil :: Vec a Zero VCons :: a -> Vec a n -> Vec a ( Succ n )

De általában csak a nagyon speciális, függő típusokkal [85] rendelkező rendszerek rendelkeznek ilyen kifejezőképességgel, amelyeket olyan nyelveken valósítanak meg, mint az Agda , Coq és mások. Például az agda nyelv szempontjából a szócikk Vec :: * -> Nat -> *azt jelentené, hogy egy típus neme a típustól Vec függNat (vagyis egyfajta elem függ egy másik, alacsonyabb fajta elemétől ).

2012 - ben elkészült a Haskell nyelv kiterjesztése [83] , amely a nemek fejlettebb rendszerét valósítja meg, és a fenti kódot helyesbíti Haskell kóddal. A megoldás az, hogy minden típust (bizonyos korlátozások mellett) automatikusan „ előléptet ” ( eng. promote ) magasabb szintre, azonos nevű nemzetségeket képezve, amelyek kifejezetten használhatók. Ebből a szempontból a bejegyzés nem függő - ez csak azt jelenti, hogy a vektor második paraméterének a megnevezett nemzetséghez kell tartoznia , és ebben az esetben ennek a nemzetségnek az egyetlen eleme az azonos nevű típus. Vec :: * -> Nat -> *Nat

A megoldás meglehetősen egyszerű, mind a fordítóprogramban való megvalósítás, mind a gyakorlati hozzáférhetőség szempontjából. És mivel a típuspolimorfizmus eleve természetes eleme Haskell szemantikájának, a típuspromóció kedves polimorfizmushoz vezet , ami egyszerre növeli a kód újrafelhasználását és magasabb szintű típusbiztonságot biztosít . Például a következő GADT -t használják a típusegyenlőség ellenőrzésére:

adatok EqReﬂ a b ahol Reﬂ :: EqReﬂ a a

a klasszikus Haskellben van egy neme * -> * -> *, ami megakadályozza, hogy a típuskonstruktorok , például a Maybe. A típuspromóción alapuló nemzetségrendszer polimorf nemzetségre következtet forall X. X -> X -> *, ami a típust EqReﬂáltalánosabbá teszi. Ezt kifejezetten le lehet írni:

adatok EqReﬂ ( a :: X ) ( b :: X ) ahol Reﬂ :: minden X . forall ( a :: X ) . EqReﬂ a a

Hatás polimorfizmus

A hatásrendszereket Gifford és Lucassen javasolta az1980-as évek második felében [86] [87] [88] azzal a céllal, hogy elkülönítsék a mellékhatásokat a biztonság és a hatékonyságpontosabb szabályozása érdekében a versenyprogramozásban .

Ebben az esetben az effektus - polimorfizmus egy adott funkció tisztaságának kvantifikálását jelenti , azaz egy jelző beillesztését a funkciótípusba , amely a funkciót tisztának vagy szennyezettnek minősíti. Ez a tipizálási kiterjesztés lehetővé teszi a magasabb rendű függvények tisztaságának elvonatkoztatását a nekik argumentumként átadott függvények tisztaságától.

Ennek különösen akkor van jelentősége, amikor a modulok ( absztrakt típusokat tartalmazó rekordok ) feletti függvényekre - funktorokra - költözünk át, mert tisztasági feltételek mellett joguk van az alkalmazhatóságra, de mellékhatások jelenlétében generálni kell a típusbiztonság érdekében . (erről bővebben lásd a típusok egyenértékűségét az ML modul nyelvében ). Így a magasabb rendű, első osztályú modulok nyelvén az effektus-polimorfizmus szükséges alapnak bizonyul a generativitási polimorfizmus támogatásához : a tisztasági jelzőt átadva egy funktornak egyetlen rendszerben választható az aplikatív és a generatív szemantika között. [65]

Támogatás programozási nyelvekben

A típusbiztos parametrikus polimorfizmus elérhető Hindley-Milner -típusú nyelveken – ML dialektusokban ( Standard ML , OCaml , Alice , F# ) és leszármazottaikban ( Haskell , Clean , Idris , Mercury , Agda ) is mint a tőlük örökölt hibrid nyelvekben ( Scala , Nemerle ).

Az általános adattípusok (generikusok) abban különböznek a parametrikusan polimorf rendszerektől, hogy korlátozott kvantifikációt használnak , ezért nem lehet 1 -nél magasabb rangú . Elérhetőek Ada , Eiffel , Java , C# , D , Rust ; és Delphiben is a 2009-es verzió óta. Először a CLU -ban jelentek meg .

Intenzív polimorfizmus

Az intenzionális polimorfizmus a parametrikus polimorfizmus összeállításának optimalizálására szolgáló technika ,amely összetett típuselméleti elemzésen alapul , amely a típusok futásidejű számításaiból áll. Az intenzív polimorfizmus lehetővé teszi a címkék nélküli szemétgyűjtést , azargumentumok függvényeknek való doboz nélküli átadását és a dobozos (memória-optimalizált) lapos adatstruktúrákat. [89] [90] [91]

Monomorfizálás

A monomorfizálás a parametrikus polimorfizmus összeállításának optimalizálására szolgáló technikahogy egy polimorf függvény vagy típus minden használati esetéhez monomorf példányt generálnakMás szavakkal, a paraméteres polimorfizmus a forráskód szintjén ad hoc polimorfizmust jelent a célplatform szintjén. A monomorfizálás javítja a teljesítményt (pontosabban a polimorfizmust "mentessé" teszi), ugyanakkor növelheti a kimeneti gépi kód méretét . [92]

Hindley - Milner

A klasszikus változatban az ML nyelv alapjául szolgáló Hindley-Milner típusú rendszer (szintén egyszerűen "Hindley-Milner" vagy "X-M", angol HM ) [93] [94] az F rendszer egy részhalmaza , amelyet a predikatívus korlátoz. prenex polimorfizmus, amely lehetővé teszi az automatikus típuskövetkeztetést , amelyhez a Hindley-Milner hagyományosan a Robin Milner által kifejlesztett ún. W [ algoritmust is magában foglalta .

Az X-M számos implementációja a rendszer továbbfejlesztett változata, amely egy „ fő tipizálási sémát ” reprezentál [93] [2] , amely egyetlen lépésben, szinte lineáris összetettséggel egyidejűleg kikövetkezi az egyes kifejezések legáltalánosabb polimorf típusait, és szigorúan ellenőrzi azok típusát. megállapodás .

Megalakulása óta a Hindley-Milner típusú rendszert többféleképpen kiterjesztették [95] . Az egyik legismertebb kiterjesztés az ad-hoc polimorfizmus támogatása típusosztályokon keresztül , amelyeket tovább általánosítanak minősített típusokra .

Az automatikus típuskövetkeztetést az ML , mint interaktív tételbizonyító rendszer, a " Logic for Computable Functions " eredeti fejlesztése során szükségesnek tartották , ezért a megfelelő korlátozásokat bevezették. Ezt követően az ML alapján számos hatékonyan lefordított általános célú nyelvet fejlesztettek ki, amelyek a nagyszabású programozásra voltak orientálva , és ebben az esetben a típuskövetkeztetés támogatásának szükségessége meredeken csökken, mivel a modul interfészek az ipari gyakorlatban mindenképpen kifejezetten a típusokkal kell ellátni [81 ] . Ezért számos Hindley-Milner kiterjesztést javasoltak, amelyek elkerülik a típuskövetkeztetést a felhatalmazás javára, egészen a teljes F rendszer támogatásáig , impredikatív polimorfizmussal, mint például a magasabb rendű modulnyelv , amely eredetileg explicit modul típusú annotáció, és számos kiterjesztéssel és dialektussal, valamint Haskell nyelvi kiterjesztéssel ( , és ). Rank2TypesRankNTypesImpredicativeTypes

A Standard ML MLton fordítója monomorfizál , de a Standard ML - re alkalmazható egyéb optimalizálás miatt a kimeneti kód ebből eredő növekedése nem haladja meg a 30%-ot [92] .

C és C++

C-ben a függvények nem első osztályú objektumok , de lehetőség van függvénymutatók definiálására , amivel magasabb rendű függvényeket építhetünk fel [96] . A nem biztonságos parametrikus polimorfizmus úgy is elérhető , hogy egy típus szükséges tulajdonságait kifejezetten átadja a nyelv egy tipizálatlan részhalmazán , amelyet egy tipizálatlan mutató képvisel nemmutatóvisszafelé A.)(a nyelvi közösségben „általános mutatónak” nevezik97][ ad-hoc polimorfizmus , mivel nem változtatja meg a mutató reprezentációját, azonban kifejezetten a fordító típusrendszerének megkerülésére van írva [96] . void* void*

Például a standard függvény qsortbármilyen típusú elem tömbjét képes kezelni, amelyhez összehasonlító függvény [96] van definiálva .

struct segment { int start ; int end ; }; int seg_cmpr ( struct segment * a , struct segment * b ) { return abs ( a -> end - a -> start ) - abs ( b -> end - b -> start ); } int str_cmpr ( char ** a , char ** b ) { return strcmp ( * a , * b ); } struct szegmens segs [] = { { 2 , 5 }, { 4 , 3 }, { 9 , 3 }, { 6 , 8 } }; char * strs [] = { "három" , "egy" , "kettő" , "öt" , "négy" }; fő () { 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 ); ... }

C-ben azonban lehetséges a tipizált parametrikus polimorfizmus idiomatikus reprodukálása void*[98] használata nélkül .

A C++ nyelv olyan sablonalrendszert biztosít, amely parametrikus polimorfizmusnak tűnik, de szemantikailag ad hoc mechanizmusok kombinációjával valósítja meg:

sablon < típusnév T > T max ( T x , T y ) { ha ( x < y ) vissza y ; más visszatér x ; } int main () { int a = max ( 10 , 15 ); dupla f = max ( 123,11 , 123,12 ); ... }

monomorfizálása C++ sablonok fordításakor elkerülhetetlen , mert a nyelv típusrendszere nem támogatja a polimorfizmust – a polimorf nyelv itt egy statikus kiegészítő a monomorf nyelvi maghoz [99] . Ez a fogadott gépi kód mennyiségének többszörös növekedéséhez vezet , amit " kódfelfújásként " [100] ismerünk .

Történelem

A parametrikus polimorfizmus jelölését a lambda-kalkulus (úgynevezett polimorf lambda-kalkulus vagy F rendszer ) továbbfejlődéseként formálisan Jean-Yves Girard [101] [102] ( 1971 ) logikus írta le , tőle függetlenül egy hasonló. rendszert John S. Reynolds informatikus írta le [103] ( 1974 ) [104] .

A paraméteres polimorfizmust először 1973-ban vezették be az ML -ben [41] [105] . Tőle függetlenül a parametrikus típusokat Barbara Liskov irányításával valósították meg a CLU -nál ( 1974 ) [41] .

Lásd még

Jegyzetek

↑ 1 2 Strachey, "Fundamental Concepts", 1967 .
↑ 1 2 Pierce, 2002 .
↑ Cardelli, Wegner, "A típusok megértéséről", 1985 , 1.3. A polimorfizmus fajtái, p. 6.
↑ 1 2 Appel, "Critique of SML", 1992 .
↑ 1 2 Jones, "A minősített típusok elmélete", 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. értekezés), 2009 , p. 91-92.
↑ 1 2 3 4 5 6 Rossberg, "1ML - Core and Modules United (F-ing First-class Modules)", 2015 .
↑ Blume, "Kivételkezelők", 2008 , p. tizenegy.
↑ Wells, 1994 .
↑ Pierce, 2002 , 22 Típusok rekonstrukciója, p. 361.
↑ Pierce, 2002 , 23.6 Törlés, tipizálhatóság és típusrekonstrukció, p. 378-381.
↑ Remy, "ML absztrakt és rekordtípusokkal", 1994 .
↑ Garrigue, Remy, "Semi-Explicit First-Class Polymorphism for ML", 1997 .
↑ Reynolds, "Programozási nyelvek elméletei", 1998 , 17. Polimorfizmus. Bibliográfiai jegyzetek, p. 393.
↑ Első osztályú polimorfizmus az MLtonon . Letöltve: 2016. július 28. Az eredetiből archiválva : 2015. november 28.. (határozatlan)
↑ Pierce, 2002 , 22.7 Polymorphism via let, p. 354-359.
↑ 1 2 3 4 5 Ohori, "Polymorphic Record Calculus and its Compilation", 1995 .
↑ Dushkin, "Monomorfizmus, polimorfizmus és egzisztenciális típusok", 2010 .
↑ Cardelli, "Tipikus programozás", 1991 , p. húsz.
↑ Pierce, 2002 , 23.10 Impredikativitás, p. 385.
↑ Pierce, 2002 , 22. fejezet. Típusrekonstrukció. 22.8. További megjegyzések, p. 361-362.
↑ Wonseok Chae (Ph.D. értekezés), 2009 , p. tizennégy.
↑ 1 2 3 Garrigue, "Polymorphic Variants", 1998 .
↑ Blume, "Bővíthető programozás első osztályú esetekkel", 2006 , p. tíz.
↑ 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, p. 3-6.
↑ Leijen, "Első osztályú címkék", 2004 , p. egy.
↑ Gaster, Jones, "Polymorphic Extensible Records and Variants", 1996 , Abstract, p. egy.
↑ 1 2 Paulson, "ML for the Working Programmer", 1996 , 2.9 Records, p. 35.
↑ 1 2 3 4 Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , 1.2 Compilation Method for Record Polymorphism, p. 6-8.
↑ Harper, "Intro to SML", 1986 .
↑ 1 2 3 Remy, "Típuskövetkeztetés rekordokhoz", 1991 , p. 2.
↑ 1 2 3 4 5 Blume, "Row polymorphism at work", 2007 .
↑ Funkcionális rekord frissítés . Letöltve: 2016. június 30. Az eredetiből archiválva : 2016. június 2. (határozatlan)
↑ 1 2 Alice ML szintaktikai fejlesztések . Letöltve: 2016. június 30. Az eredetiből archiválva : 2016. november 27.. (határozatlan)
↑ Funkcionális rekordbővítés és sorrögzítés . Letöltve: 2016. június 30. Az eredetiből archiválva : 2016. augusztus 13.. (határozatlan)
↑ Harper, Pierce, "Record calculus based on symmetric concatenation", 1991 .
↑ 1 2 Wand, "Típuskövetkeztetés rekordösszefűzéshez és többszörös öröklődéshez", 1991 .
↑ 12 Sulzmann , 1997 .
↑ 1 2 3 4 Pierce, 2002 , 1.4 Rövid történelem, p. 11-13.
↑ Remy, "Típuskövetkeztetés rekordokhoz", 1991 , p. 2-3.
↑ 1 2 3 4 5 6 7 Leijen, "First-class Labels", 2004 , 1. o. 13-14.
↑ Cardelli, "A többszörös öröklődés szemantikája", 1988 .
↑ Cardelli, Wegner, "A típusok megértéséről", 1985 .
↑ Pierce, 2002 , 16. Altípus-metaelmélet, p. 225.
↑ Pierce, 2002 , 11.8 Felvételek, p. 135.
↑ 1 2 3 Minsky fordította: DMK, 2014 , Altípusozás és szövegközi polimorfizmus, p. 267-268.
↑ Pálca, "Típuskövetkeztetés objektumokhoz", 1987 .
↑ 1 2 Minsky fordítása: DMK, 2014 , Tárgypolimorfizmus, p. 255-257.
↑ 1 2 Remy, "Típuskövetkeztetés rekordokhoz", 1991 , Kapcsolódó munka, p. 3.
↑ 1 2 Remy, "Type Inference for Records", 1991 .
↑ Blume, "Bővíthető programozás első osztályú esetekkel", 2006 , p. tizenegy.
↑ Remy, "Subtypes and Row polymorphism", 1995 .
↑ 1 2 Remy, Vouillon, "Objective ML", 1998 .
↑ Pierce, 2002 , 15.8 További megjegyzések, p. 223.
↑ Minsky fordítása: DMK, 2014 , Polimorf változatok, p. 149-158.
↑ Pierce, 2002 , 24 Egzisztenciális típusok, p. 404.
↑ 1 2 Reynolds, "Programozási nyelvek elméletei", 1998 , 18. Modulspecifikáció, p. 401-410.
↑ Cardelli, "Tipikus programozás", 1991 , 4.4. Tuple típusok, p. 20-23.
↑ 1 2 Harper, Lillibridge, "Típuselméleti megközelítés a magasabb rendű modulokhoz megosztással", 1993 .
↑ 1 2 3 4 Yallop, fehér, "Könnyű, magasabb fajtájú polimorfizmus", 2014 .
↑ Harper, Mitchell, "Type Structure of SML", 1993 .
↑ Rossberg, "1ML - Core and Modules United (F-ing First-class Modules)", 2015 , Impredicativity Reloaded, p. 6.
↑ 1 2 Rossberg, "1ML speciális effektusokkal (F-ing Generativity Polymorphism)", 2016 .
↑ Ohori, "Compilation Method for Polymorphic Record Calculi", 1992 .
↑ Ohori - SML# (bemutató) (downlink) . Letöltve: 2016. június 30. Az eredetiből archiválva : 2016. augusztus 27.. (határozatlan)
↑ Ohori, "Polymorphic Record Calculus and its Compilation", 1995 , p. 38.
↑ 1 2 Blume, "Bővíthető programozás első osztályú esetekkel", 2006 , p. 9.
↑ Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , 5 Implementaion, p. 37.
↑ 1 2 3 4 5 Blume, "Bővíthető programozás első osztályú esetekkel", 2006 .
↑ Gaster (Ph.D. értekezés), 1998 .
↑ Leijen, "Első osztályú címkék", 2004 , p. 7.
↑ Leijen, "First-class Labels", 2004 .
↑ Bővíthető rekordok a Haskell-Wikin (lefelé mutató link)
↑ Blume személyes oldala . Letöltve: 2016. június 30. Az eredetiből archiválva : 2016. május 19. (határozatlan)
↑ Blume, "Kivételkezelők", 2008 .
↑ 1 2 3 Wonseok Chae (Ph.D. értekezés), 2009 .
↑ Paulson, "ML for the Working Programmer", 1996 , 4.6 Kivételek deklarálása, p. 135.
↑ Harper, "Programozási nyelvek gyakorlati alapjai", 2012 , 28.3 Kivétel típusa, p. 258-260.
↑ 1 2 ML2000 előzetes tervezés, 1999 .
↑ Harper, "Practical Foundations for Programming Languages", 2012 , 22. fejezet. Konstruktorok és fajták, 1. o. 193.
↑ 1 2 3 Weirich et al, "Giving Haskell a promóció", 2012 .
↑ Fluet, Pucella, "Phantom Types and Subtyping", 2006 .
↑ Pierce, 2002 , 30.5 Továbblépve: Függő típusok, p. 489-490.
↑ Gifford, Lucassen, "Effect systems", 1986 .
↑ Lucassen, Gifford, "Polymorphic Effect Systems", 1988 .
↑ Talpin, Jouvelot, 1992 .
↑ Harper, Morrisett, "Intensional Type Analysis", 1995 .
↑ Crary, Weirich, Morrisett, "Intensional polymorphism", 1998 .
↑ Pierce, 2002 , 23.2. A polimorfizmus fajtái, o. 364-365.
↑ 1 2 hét, "Whole-Program Compilation in MLton", 2006 .
↑ 1 2 Hindley, "Principal Type Scheme", 1969 .
↑ Milner, "A típuspolimorfizmus elmélete", 1978 .
↑ Jones, "FP túlterheléssel és HO-polimorfizmussal", 1995 .
↑ 1 2 3 Kernighan B. , Ritchie D. A C programozási nyelv = A C programozási nyelv. - 2. kiadás - Williams , 2007. - S. 304. - ISBN 0-13-110362-8 . , 5.11. Funkciómutatók
↑ Appel, "Critique of SML", 1992 , p. 5.
↑ Oleg Kiszeljov. Valóban polimorf listák C-ben . okmij.org. Letöltve: 2016. november 22. Az eredetiből archiválva : 2017. január 30. (határozatlan)
↑ Mitchell, "Concepts in Programming Languages", 2004 , 6.4. Polimorfizmus és túlterhelés, p. 145-151.
↑ Scott Meyers . Kódfelfújás a sablonok miatt . comp.lang.c++.moderated . Usenet (2002. május 16.). Letöltve: 2010. január 19. (határozatlan)
↑ Girard, "Extension of Type Theory", 1971 .
↑ Girard, "Magasabb rendű kalkulus", 1972 .
↑ Reynolds, "Theory of Type Structure", 1974 .
↑ Pierce, 2002 , 23.3 System F, p. 365-366.
↑ Milner et al, "LCF", 1975 .

Irodalom

Christopher Strachey. A programozási nyelvek alapfogalmai . - 1967. Archiválva : 2017. augusztus 12.
- Újra kiadva: Christopher Strachey. A programozási nyelvek alapfogalmai // Magasabb rendű és szimbolikus számítás . - 2000. - T. 13 . - S. 11-49 . - doi : 10.1023/A:1010000313106 .

J Roger Hindley. Egy objektum fő típussémája a kombinatív logikában // Transactions of the American Mathematical Society . - American Mathematical Society, 1969. - Vol. 146 . - P. 29-60 . - doi : 10.2307/1995158 .

Jean-Yves Girard. Une Extension de l'Interpretation de Gödel à l'Analysis, et son Application à l'Élimination des Coupures dans l'Analysis et la Théorie des Types (francia) // Proceedings of the Second Scandinavian Logic Symposium. - Amszterdam, 1971. - P. 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 (francia) . – Université Paris 7, 1972.

John C. Reynolds. A típusszerkezet elmélete felé // Számítástechnikai előadásjegyzetek . - Párizs: Colloque sur la programation, 1974. - 19. évf . - S. 408-425 . - doi : 10.1007/3-540-06859-7_148 .

Milner R. , Morris L., Newey M. Logic for Computable Functions with reflexive and polymorphic type // Arc-et-Senans. — Proc. Konferencia a bizonyító és javító programokról, 1975.

Robin Milner . A típuspolimorfizmus elmélete a programozásban. - 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. Operations on Records // Matematikai struktúrák a számítástechnikában. - 1991. -1.,szám. 1.

Luca Cardelli , Peter Wegner. A típusok, az adatabsztrakció és a polimorfizmus megértése //ACM számítástechnikai felmérések. - New York, USA:ACM, 1985. -17,no. 4. -S. 471-523. —ISSN 0360-0300. -doi:10.1145/6041.6042.

Robert Harper . Bevezetés a Standard ML-be. - Carnegie Mellon Egyetem, 1986. - 97 p. — ISBN PA 15213-3891. (Orosz)

John M. Lucassen, David K. Gifford. Funkcionális és kötelező programozás integrálása . – 1986.

Luca Cardelli . Alapvető polimorf típusellenőrzés. – 1987.

Mitchell Wand . Complete Type Inference for Simple Objects // In Proc. 2. IEEE szimpózium a logikáról a számítástechnikában. - 1987. -P. 37-44.

Martín Abadi, Luca Cardelli , Pierre-Louis Curien. Formális paraméteres polimorfizmus . – POPL, 1993.

Luca Cardelli . A többszörös öröklődés szemantikája // Inf. Comput. 76. - 1988. -P. 138-164.

John M. Lucassen, David K. Gifford. Polimorf hatásrendszerek . – POPL , 1988.

Didier Remy. Type Inference for Records in a natural Extension of ML // Research Report 1431. - Institut National de Recherche en Informatique et Automatisme, 1991.

Luca Cardelli . Tipikus programozás // IFIP State-of-the-art jelentések. - New York: Springer-Verlag, 1991. -Iss. A programozási fogalmak formális leírása. -P. 431-507.

Robert Harper , Benjamin Pierce. Számítás rögzítése szimmetrikus összefűzés alapján // CMU-CS-90-157R. – Carnegie Mellon Egyetem, a Naval Research által támogatott és felügyelt, 1991.

Mitchell Wand . Típuskövetkeztetés rekordösszefűzéshez és többszörös öröklődéshez // Válogatás az 1989-es IEEE szimpóziumból: Logic in Computer Science. - Információ és számítás, 1991. -T. 93,sz. 1. -doi:10.1016/0890-5401(91)90050-C.

Andrew W. Appel. A Standard ML kritikája . – Princetoni Egyetem, 1992.

Mark P. Jones. A minősített típusok elmélete . – ESOP , Springer-Verlag számítástechnikai előadásjegyzetek, 1992.

Atsushi Ohori. A Compilation Method for ML-Style Polymorphic Record Calculi // POPL: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages,. - Kyoto University, ACM , 1992. - S. 154-165 . - doi : 10.1.1.105.7655 .

J.P. Talpin, P. Jouvelot. Polimorf típus, régió és hatás következtetés // 2(3):245271. – JFP , 1992.

Robert Harper , John C. Mitchell. A szabványos ML típusszerkezetéről. -ACMTOPLAS, 1993. -S. 211-252.

Robert Harper , Mark Lillibridge. Típuselméleti megközelítés a magasabb rendű modulokhozmegosztással . -ACMPress,POPL, 1993. - ISBN CMU-CS-93-197. -doi:10.1.1.14.3595.

Didier Remy. Objektumok programozása ML-ART segítségével: Az ML kiterjesztése absztrakt és rekordtípusokkal . - International Symposium on Theoretical Aspects of Computer Software, Springer-Verlag, 1994. - P. 321-346 .

JB Wells. A tipizálhatóság és a típusellenőrzés a másodrendű lambda-számításban egyenértékű és eldönthetetlen // Proceedings of the 9th Annual IEEE . - Symposium on Logic in Computer Science (LIS), 1994. - P. 176-185 .

Robert Harper , . Polimorfizmus összeállítása intenzionális típusanalízis segítségével. – 1995.

Atsushi Ohori. Polimorf rekordszámítás és összeállítása . - Kyoto University, ACM , 1995. - S. 844-895 .

Mark P. Jones. Funkcionális programozás túlterheléssel és magasabb rendű polimorfizmussal . - Springer-Verlag Lecture Notes, 1995. - doi : 10.1.1.26.9460 .

Didier Remy. Better Subtypes and Row Variables for Record Types // Bemutatták az Advances in Types for Computer Science at the Newton Institute workshopon. – Cambridge, Egyesült Királyság, 1995.

Lawrence C. Paulson . ML a Working Programmer számára. — 2. - Cambridge, Nagy-Britannia: Cambridge University Press, 1996. - 492 p. -ISBN 0-521-57050-6(keménykötés), 0-521-56543-X (puhakötés).

Benedict R. Gaster, Mark P. Jones. Polimorf típusú rendszer bővíthető rekordokhoz és változatokhoz // Műszaki jelentés NOTTCS-TR-96-3. – Nottinghami Egyetem, 1996.

Jacques Garrigue, Didier Remy. Félig explicit első osztályú polimorfizmus az ML számára // Academic Press. — Információ és számítás, 1997.

M. Sulzmann. Nyilvántartási rendszerek tervezése // Műszaki jelentés YALEU/DCS/RR-1128. - Yale Egyetem, 1997. - doi : 10.1.1.17.6563 .

Karl Crary, Stephanie Weirich, J. Gregory Morrisett. Intenzív polimorfizmus a típustörlés szemantikában . – ICFP , 1998.

Benedict R. Gaster. Feljegyzések, változatok és minősített típusok // Műszaki jelentés NOTTCS-TR-98-3. – Ph.D. Szakdolgozat, 1998.

Jacques Garrigue. Programozás polimorf változatokkal . – Kiotói Egyetem, 1998.

Didier Rémy, Jérome Vouillon. Objective ML: Az ML hatékony objektumorientált kiterjesztése . - Az objektumrendszerek elmélete és gyakorlata, ACM , 1998. - V. 4 (1) . - S. 27-50 .

John C. Reynolds. Programozási nyelvek elméletei . - Cambridge University Press, 1998. - ISBN 978-0-521-59414-1 (keménykötés), 978-0-521-10697-9 (puhakötés).

Az ML2000 munkacsoport. Az ML2000 alapelvei és előzetes terve . – 1999.

Benjamin Pierce. Típusok és programozási nyelvek . - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Orosz nyelvű fordítás: Benjamin Pierce. Típusok programozási nyelvekben. - Dobrosvet , 2012. - 680 p. — ISBN 978-5-7913-0082-9 .

John C. Mitchell Fogalmak a programozási nyelvekben. - Cambridge University Press, 2004. - ISBN 0-511-04091-1 (e-könyv a netLibrary-ben); 0-521-78098-5 (keménykötés).

Jens Palsberg, Tian Zhao. Típuskövetkeztetés rekordösszefűzéshez és altípushoz . - 2004. Archiválva : 2016. szeptember 16.

Daan Leijen. Első osztályú címkék bővíthető sorokhoz // TechReport UU-CS-2004-51. – Utrechti Egyetem, 2004.

Matthias Blume, Umut A. Acar, Wonseok Chae. Bővíthető programozás első osztályú esetekkel . – ICFP , 2006.

Matthew Fluet, Riccardo Pucella. Fantomtípusok és altípusok . – JFP , 2006.

Stephen Weeks. Teljes program összeállítása MLton nyelven . - 2006. Archiválva : 2007. június 29.

Matthias Blume. Feljegyzések, összegek, esetek és kivételek: Sorpolimorfizmus a munkahelyen : beszédvideó. – Microsoft, 2007.

Matthias Blume, Umut A. Acar, Wonseok Chae. Kivételkezelők, mint bővíthető esetek . - Toyota Technológiai Intézet Chicagóban, APLAS, 2008.

Wonseok Chae. Típus Biztonságos bővíthető programozás // Ph.D. tézis. – Chicagói Toyota Technológiai Intézet, 2009.

Római Dushkin. Monomorfizmus, polimorfizmus és egzisztenciális típusok . – 2010.

Jeremy Yallop, Leo White. Könnyű, magasabb típusú polimorfizmus . — Nemzetközi Funkcionális és Logikai Programozási Szimpózium, 2014.

Robert Harper . Programozási nyelvek gyakorlati alapjai. - 1.37-es verzió (2014.11.01.) - a Creative Commons Nevezd meg!-Nem kereskedelmi-Nincsenek származtatott munkák 3.0 Egyesült Államok licence alapján licencelve., 2012. - 544 p. Archiválva: 2015. október 24. aWayback Machine

Stephanie Weirich, Brent A. Yorgey, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis és Jose P. Magalhães. Haskell előléptetése // In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation. - NY, USA: TLDI , 2012. - S. 53-66 .

Minsky, Madhavapeddy, Hickey. Valós világ OCaml: Funkcionális programozás tömegek számára . - O'Reilly Media, 2013. - 510 p. — ISBN 9781449324766 .
- Orosz nyelvű fordítás:
  Minsky, Madhavapeddy, Hickey. Programozás OCaml nyelven . - DMK, 2014. - 536 p. - ISBN 978-5-97060-102-0 . (Orosz)

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

Andreas Rossberg. 1 ML speciális effektusokkal (F-ing Generativity Polymorphism) . – WadlerFest, Google, 2016.

Haskell-Wiki: Egzisztenciális típusok . (határozatlan)

Haskell-Wiki: Rank-N típusok . (határozatlan)

Haskell-Wiki: Impredikatív típusok . (határozatlan)

Jacques Garrigue. OCaml kézikönyv: Polimorf változatok . (határozatlan)

Adattípusok
Értelmezhetetlen	Bit Rágcsál Byte qubit Csemege Jellemvonás Szó
Numerikus	Egész fix pont lebegőpont Racionális Összetett Hosszú intervallum
Szöveg	Szimbolikus Húr
Referencia	Cím Link Mutató Csomagolás
Összetett	Algebrai adattípus ( általános ) Osztály Típus-termék ( Írj Tuple szerkezet ) Egy tárgy Konszolidáció ( címkézett ) Rendelt pár
absztrakt	sor Lista Fordulat Kazal Asszociatív tömb (megjelenítés, térkép ) Sok multiset típus Grafikon
Egyéb	Logikus Alsó Magasabb Polimorf Funkcionális felsorolható Gyűjtemény Kivétel nemzetség ( metaosztály ) Monád Szemafor Folyam üres
Kapcsolódó témák	Absztrakt adattípus primitív típus Adatstruktúra Generikus típusú változó Felület Konstruktor (OOP) Konstruktor (FP) Konstruktor típusa Típusöntés Prototípus Típusrendszer