Parametrinen polymorfismi

Kokeneet kirjoittajat eivät ole vielä tarkistaneet sivun nykyistä versiota, ja se voi poiketa merkittävästi 12. huhtikuuta 2021 tarkistetusta versiosta . tarkastukset vaativat 5 muokkausta .

Parametrinen polymorfismi ohjelmointikielissä ja tyyppiteoriassa on tyyppijärjestelmän semantiikan ominaisuus, jonka avulla voit käsitellä erityyppisiä arvoja samalla tavalla, eli suorittaa fyysisesti saman koodin erityyppisille tiedoille [1] [2] .

Parametrista polymorfismia pidetään polymorfismin "todellisena" muotona [ 3] , mikä tekee kielestä ilmaisuvoimaisemman ja lisää huomattavasti koodin uudelleenkäyttöä . Perinteisesti se vastustaa ad-hoc-polymorfismia [1] , joka tarjoaa yhden rajapinnan mahdollisesti eri koodille tietyssä kontekstissa sallituille eri tyypeille, mahdollisesti yhteensopimattomille ( staattisesti tai dynaamisesti ). Useissa laskelmissa, kuten pätevien tyyppien teoriassa , ad-hoc-polymorfismia käsitellään parametrisen polymorfismin erikoistapauksena.

Parametrinen polymorfismi on ML -perheen kielten tyyppijärjestelmien taustalla ; tällaisia järjestelmiä kutsutaan polymorfisiksi. Kielten yhteisöissä, joissa on ei-polymorfisia tyyppijärjestelmiä ( Algolin ja BCPL: n [4] jälkeläisiä ), parametrisesti polymorfisia toimintoja ja tyyppejä kutsutaan " yleistetyiksi ".

Tyyppipolymorfismi

Termiä " parametrinen polymorfismi " käytetään perinteisesti viittaamaan tyyppiturvalliseen parametriseen polymorfismiin, vaikka siitä on olemassa myös tyypittämättömiä muotoja (ks. parametrinen polymorfismi kielessä C ja C++ ) [4] . Tyyppiturvallisen parametrisen polymorfismin avainkäsite polymorfisen funktion lisäksi on polymorfinen tyyppi .

Polymorfinen tyyppi ( eng. polymorphic type ) tai polytyyppi ( eng. polytype ) on toisen tyypin parametroima tyyppi. Tyyppikerroksen parametria kutsutaan tyyppimuuttujaksi (tai tyyppimuuttujaksi) .

Muodollisesti tyyppipolymorfismia tutkitaan polymorfisesti tyypitetyssä lambda-laskennassa , nimeltään System F.

Esimerkiksi funktio, joka appendketjuttaa kaksi listaa yhdeksi, voidaan rakentaa listaelementtien tyypistä riippumatta. Kuvaa tyyppimuuttujan listan elementtien tyyppi . Sitten funktio voidaan kirjoittaa muodossa " " (tässä konstruktio tarkoittaa tyyppiä " lista, jonka jokaisella elementillä on tyyppi " - Haskell-kielessä käytetty syntaksi ). Tässä tapauksessa tyypin sanotaan olevan parametroitu muuttujalla kaikille arvoille . Jokaisessa tiettyjen argumenttien sovelluskohdassa arvo ratkaistaan, ja jokainen maininta siitä tyyppiallekirjoituksessa korvataan arvolla, joka vastaa sovelluksen kontekstia. Näin ollen tässä tapauksessa funktiotyypin allekirjoitus edellyttää, että molempien listojen ja tuloksen elementtityypit ovat identtisiä .aappendforall a. [a] × [a] -> [a][a]aaaappenda

Tyyppimuuttujan kelvolliset arvot saadaan kvantifioinnilla . Yksinkertaisimmat kvantisoijat ovat universaaleja (kuten esimerkissä append) ja eksistentiaalisia (katso alla).

Hyväksytty tyyppi on polymorfinen tyyppi, joka on lisäksi varustettu joukolla predikaatteja , jotka säätelevät tämän tyyppisen parametrin kelvollisten arvojen aluetta. Toisin sanoen tyyppihyväksynnän avulla voit hallita kvantifiointia mielivaltaisella tavalla. Hyväksyttyjen tyyppien teorian rakensi Mark P. Jones vuonna 1992 [5] . Se tarjoaa yhteisen perustelun eksoottisimpiin tyyppijärjestelmiin, mukaan lukien tyyppiluokat , laajennettavat merkinnätja alatyypit , ja mahdollistaa erityisten rajoitusten täsmällisen muotoilun tietyille polymorfisille tyypeille, mikä muodostaa suhteen parametrisen ja ad-hoc- suhteen välillä. polymorfismi ( ylikuormitus ) sekä eksplisiittisen ja implisiittisen ylikuormituksen välillä. Tyypin assosiaatiota predikaattiintässä teoriassa kutsutaan todisteeksi . Lambda-laskennan kaltainen algebra , mukaan lukien todisteiden abstraktio, todisteiden soveltaminen jne. Tämän algebran termin korrelointia eksplisiittisesti ylikuormitetun funktionkanssa kutsutaan todisteiden käännökseksi .

Motivoivia esimerkkejä yleisen teorian kehittämiselle olivat Wadler-Blott-tyyppiluokat ja laajennettavien tietueiden tyypitys Harper-Pearce-predikaattien avulla [5] [6] .

Polymorfisten järjestelmien luokittelu

Parametrisesti polymorfiset järjestelmät luokitellaan pohjimmiltaan arvon ja predikatiivisen ominaisuuden mukaan . Lisäksi erotetaan eksplisiittinen ja implisiittinen polymorfismi [7] ja joukko muita ominaisuuksia. Implisiittinen polymorfismi saadaan aikaan tyyppipäätelmän avulla , mikä parantaa huomattavasti käytettävyyttä, mutta jolla on rajallinen ilmaisukyky. Monet käytännön parametrisesti polymorfiset kielet erottavat ulkoisen implisiittisesti kirjoitetun kielen ja sisäisen eksplisiittisesti kirjoitetun kielen vaiheet .

Yleisin polymorfismin muoto on " korkeamman asteen impredikatiivinen polymorfismi ". Tämän muodon suosituimpia rajoituksia ovat ykkösluokan polymorfismi, jota kutsutaan " prenex " ja predikatiivinen polymorfismi . Yhdessä ne muodostavat " predikatiivisen prenex - polymorfismin " , joka on samanlainen kuin ML : ssä ja aiemmissa Haskellin versioissa toteutettu .

Tyyppijärjestelmien monimutkaistuessa tyyppiallekirjoituksista tulee niin monimutkaisia, että monet tutkijat pitävät niiden täydellistä tai lähes täydellistä johtamista kriittisenä ominaisuutena, jonka puuttuminen tekee kielestä käyttökelvottoman [8] [9] . Esimerkiksi perinteisessä kombinaattorissa maptäyden tyypin allekirjoitus (ottaen huomioon yleinen kvantifiointi) tyyppiturvallisen poikkeusvirran seurannassa on seuraavassa muodossa [10] [8] (kuten edellä , tarkoittaa luetteloa tyypin elementit ):[a]a
$val\;kartta\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 \ oikea]{\xrightarrow {\gamma }}\left[\beta \right]\;)$

Sijoitus

Polymorfismin arvo osoittaa järjestelmän puitteissa sallittujen tyyppimuuttujien kvantorien sisäkkäisyyden syvyyden. " K-arvon polymorfismi " (jos k > 1 ) mahdollistaa tyyppimuuttujien määrittämisen polymorfisten arvotyyppien mukaan , joka ei ole korkeampi kuin ( k - 1) . " Korkeamman asteen polymorfismi " mahdollistaa tyyppimuuttujien kvantisoijien asettamisen mielivaltaisen määrän nuolia vasemmallekorkeamman asteen tyypeissä .

Joe Wells osoitti [ 11] , että Curry - tyyppisen System F : n tyyppipäätelmä ei ole päätettävissä yli 2:n sijalle, joten eksplisiittistä tyyppimerkintää on käytettävä korkeampia arvoja käytettäessä [12] .

On olemassa osittaisia päättelytyyppisiä järjestelmiä , jotka vaativat vain ei-johdannaisten tyyppimuuttujien merkitsemistä [13] [14] [15] .

Prenex-polymorfismi

Sijoitusluokan 1 polymorfismia kutsutaan usein prenex- polymorfiksi (sanasta "prenex" - katso prenex-normaalimuoto ). Prenex-polymorfisessa järjestelmässä tyyppimuuttujia ei voida ilmentää polymorfisilla tyypeillä. Tämä rajoitus tekee eron monomorfisten ja polymorfisten tyyppien välillä olennaisen tärkeäksi, minkä vuoksi prenex-järjestelmässä polymorfisia tyyppejä kutsutaan usein " tyypitysskeemoiksi " ( englanninkielisiksi tyypeiksi ) niiden erottamiseksi "tavallisista" (monomorfisista) tyypeistä (monotyypeistä). Tästä johtuen kaikki tyypit voidaan kirjoittaa muodossa, kun kaikki tyyppimuuttujan kvantorit sijoitetaan uloimpaan (prenex) asemaan, jota kutsutaan prenex-normaalimuodoksi . Yksinkertaisesti sanottuna polymorfisten funktioiden määrittelyt ovat sallittuja, mutta polymorfisia funktioita ei voida välittää argumenteiksi muille funktioille [16] [17] - polymorfisesti määritellyt funktiot on esitettävä monotyyppisinä ennen käyttöä.

Läheinen vastine on Damas-Milnerin niin kutsuttu " Let-polymorfismi " tai " ML - tyylinen polymorfismi ". Teknisesti Let-polymorfismissa ML :ssä on lisäsyntaktisia rajoituksia, kuten " arvorajoitus ", joka liittyy tyyppiturvaongelmiin käytettäessä viittauksia (jotka eivät esiinny puhtaissa kielissä, kuten Haskell ja Clean ) [18] [19] .

Predikatiivisuus

Predikatiivinen polymorfismi

Predikatiivinen (ehdollinen) polymorfismi edellyttää, että tyyppimuuttuja instantioidaan monotyypillä (ei polytyypillä).

Predikatiivisiin järjestelmiin kuuluvat intuitionistinen tyyppiteoria ja Nuprl .

Impredikatiivinen polymorfismi

Impredikatiivinen (ehdoton) polymorfismi mahdollistaa tyyppimuuttujan ilmentämisen mielivaltaisella tyypillä - sekä monomorfisella että polymorfisella, mukaan lukien määritettävä tyyppi. (Se, että järjestelmän sallitaan sisällyttää itsensä rekursiivisesti itseensä, kutsutaan impredikatiivisuudeksi . Mahdollisesti tämä voi johtaa paradokseihin, kuten Russell tai Cantor [20] , mutta näin ei tapahdu monimutkaisen tyyppisen järjestelmän tapauksessa [21] .)

Impredikatiivisen polymorfismin avulla voit siirtää polymorfisia funktioita muille funktioille parametreiksi, palauttaa ne tuloksena, tallentaa ne tietorakenteisiin jne., minkä vuoksi sitä kutsutaan myös ensimmäisen luokan polymorfisiksi . Tämä on polymorfismin tehokkain muoto, mutta toisaalta se aiheuttaa vakavan ongelman optimoinnissa ja tekee tyyppipäätelmästä ratkaisemattoman .

Esimerkki impredikatiivisesta järjestelmästä on System F ja sen laajennukset (katso lambda-kuutio ) [22] .

Rekursiotuki

Perinteisesti ML :n jälkeläisissä funktio voi olla polymorfinen vain "ulkopuolelta" katsottuna (eli sitä voidaan soveltaa erityyppisiin argumentteihin), mutta sen määritelmä voi sisältää vain monomorfisen rekursion (eli tyypin resoluutio on tehty ennen puhelua). ML-tyypin rekonstruoinnin laajentaminen rekursiivisiin tyyppeihin ei aiheuta vakavia vaikeuksia. Toisaalta tyyppirekonstruktion yhdistäminen rekursiivisesti määriteltyihin termeihin luo vaikean ongelman, joka tunnetaan nimellä polymorfinen rekursio . Mycroft ja Meertens ehdottivat polymorfista tyypityssääntöä, jonka avulla rekursiiviset kutsut rekursiiviseen funktioon omasta kehostaan voidaan ilmentää eri tyypeillä. Tässä Milner-Mycroft-laskennassa tunnetussa laskennassa tyyppipäätelmä on ratkaisematon . [23]

Rakenteellisen tyypin polymorfismi

Tuotetyypit (tunnetaan myös nimellä " tietueet ") toimivat olio- ja modulaarisen ohjelmoinnin muodollisena perustana. Niiden kaksoispari koostuu summatyypeistä (tunnetaan myös nimellä " variantit ") [24] [25] [19] :

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

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

Yhdessä ne ovat keino ilmaista monimutkaisia tietorakenteita ja joitain ohjelmien toiminnan näkökohtia .

Tietuelasku on yleisnimitys ongelmalle ja useille sen ratkaisuille, jotka koskevat tuotetyyppien joustavuutta ohjelmointikielissä tyyppiturvallisuuden ehdolla [26] [27] [28] . Termi ulottuu usein summatyyppeihin, ja " tietuetyypin " käsitteen rajatvoivat vaihdella laskelmista toiseen (samoin kuin itse " tyypin " käsite). Termejä " tietuepolymorfismi " (joka taas usein sisältää muunnelman polymorfia ) [27] , " moduulilaskenta " [9] ja " rakennepolymorfia " käytetään myös.

Yleistä tietoa

Tyyppituotteet ja -summat ( tietueet ja muunnelmat [ en ] tarjoavat joustavuutta monimutkaisten tietorakenteiden rakentamiseen, mutta monien tosielämän tyyppisten järjestelmien rajoitukset estävät usein niiden käytön olevan todella joustavaa. Nämä rajoitukset johtuvat yleensä tehokkuudesta, tyyppipäätelmästä tai yksinkertaisesti käytettävyydestä. [29]

Klassinen esimerkki on Standard ML , jonka tyyppijärjestelmää on tarkoituksella rajoitettu juuri sen verran , että toteutuksen helppous yhdistyy ilmaisuun ja matemaattisesti todistettavaan tyyppiturvallisuuteen .

Esimerkki tietueen määrittelystä :

> val r = { nimi = "Foo" , käytetty = tosi }; (* val r : {nimi : merkkijono, käytetty : bool} = {nimi = "Foo", käytetty = tosi} *)

Pääsy kentän arvoon sen nimellä tapahtuu lomakkeen etuliiterakenteen avulla #field record:

> val r1 = #nimi r ; (* val r1 : string = "Foo" *)

Seuraava tietueen päällä oleva funktion määritelmä on oikea:

> hauska nimi1 ( x : { nimi : merkkijono , ikä : int }) = #nimi x

Ja seuraava luo kääntäjävirheen, jonka tyyppiä ei ole täysin ratkaistu :

> hauska nimi2 x = #nimi x (* ratkaisematon tyyppi ilmoituksessa: {nimi : '1, ...} *)

Tietueiden monomorfismi tekee niistä joustamattomia, mutta tehokkaita [30] : koska kunkin tietuekentän todellinen muistipaikka tiedetään etukäteen (käännöshetkellä), siihen nimeäminen käännetään suoraan indeksointiin, joka yleensä lasketaan yhdellä koneella. ohje. Monimutkaisia skaalautuvia järjestelmiä kehitettäessä on kuitenkin toivottavaa kyetä abstraktimaan kenttiä tietyistä tietueista - esimerkiksi määrittelemään universaali kenttävalitsin:

hauska valinta r l = #l r

Mutta polymorfisen pääsyn kokoaminen kenttiin, jotka voivat olla eri järjestyksessä eri tietueissa, on vaikea ongelma sekä toimintojen turvallisuuden valvonnan kannalta kielitasolla että suorituskyvyn kannalta konekooditasolla. Naiivi ratkaisu voisi olla etsiä sanakirjaa dynaamisesti jokaisen kutsun yhteydessä (ja komentosarjakielet käyttävät sitä), mutta tämä on ilmeisesti erittäin tehotonta. [31]

Tyyppisummat muodostavat haaralausekkeen perustan , ja tyyppijärjestelmän tiukkuuden vuoksi kääntäjä hallitsee jäsentämisen täydellisyyttä. Esimerkiksi seuraavalle summatyypille :

tietotyyppi 'a foo = A of 'a | B / ( 'a * 'a ) | C

mikä tahansa sen päällä oleva toiminto näyttää

hauska baari ( p : 'a foo ) = tapaus p A x = > ... | B ( x , y ) => ... | c => ...

ja kun jokin lauseista poistetaan, kääntäjä antaa varoituksen (" match nonexhaustive"). Tapauksissa, joissa vain muutama monista vaihtoehdoista vaatii analyysiä tietyssä kontekstissa, on mahdollista järjestää default-haarautuminen ns. "Joker" - universaali näyte, jonka kanssa kaikki kelvolliset (kirjoituksen mukaan) arvot ovat vertailukelpoisia. Se on kirjoitettu alaviivalla (" _"). Esimerkiksi:

hauska baari ( p : 'a foo ) = C : n tapaus p => ... | _ => ...

Joissakin kielissä ( standardissa ML :ssä, Haskellissa ) jopa "yksinkertaisempi" rakenne if-then-elseon vain syntaktinen sokeri haaroittamisen erikoistapauksessa , eli ilmaisussa.

jos A niin B muu C

jo kieliopillisen analyysin vaiheessa esitetään muodossa

tositapaus A = > B | _ väärin => C

tai

tositapaus A = > B | _ _ => C

Syntaktinen sokeri

Standard ML :ssä tietueet ja muunnelmat ovat monomorfisia, mutta syntaktista sokeria useiden kenttien tietueiden käsittelyyn tuetaan, jota kutsutaan " universaaliksi malliksi " [32] :

> val r = { nimi = "Foo" , käytetty = tosi }; (* val r : {nimi : merkkijono, käytetty : bool} = {nimi = "Foo", käytetty = tosi} *) > val { käytetty = u , ...} = r ; (* arvo u : bool = tosi *)

" "-tyypin ellipsi {used, ...}tarkoittaa, että tässä tietueessa on muitakin kenttiä mainittujen lisäksi. Tietuepolymorfismia sinänsä ei kuitenkaan ole (ei edes esiliite ): monomorfisen tietuetyyppitiedon täysi staattinen resoluutio ( päätelmän tai eksplisiittisen huomautuksen kautta ) vaaditaan.

Tietueiden laajennus ja toiminnallinen päivitys

Termiä laajennettavat tietueet käytetään yleistäen sellaiset toiminnot kuin laajentaminen (uusi tietueen rakentaminen olemassa olevan tietueen perusteella lisäämällä uusia kenttiä), leikkaaminen (määrätyn osan ottaminen olemassa olevasta tietueesta) jne. Erityisesti se tarkoittaa ns. " funktionaalisen tietueen päivityksen " ( functional record update ) mahdollisuutta - operaatiota, jolla muodostetaan uusi tietuearvo olemassa olevan perusteella kopioimalla sen kenttien nimet ja tyypit, joissa yksi tai useampi kentti uusi tietue saa uusia arvoja, jotka eroavat alkuperäisistä (ja joilla on mahdollisesti eri tyyppi). [33] [34] [19] [35] [36] [37]

Toiminnalliset päivitys- ja laajennusoperaatiot ovat itsessään ortogonaalisia polymorfismin tallentamiseen, mutta niiden polymorfinen käyttö on erityisen kiinnostavaa. Jopa monomorfisten tietueiden kohdalla on tärkeää pystyä jättämään pois nimenomainen maininta kentistä, jotka kopioidaan muuttumattomina, ja tämä edustaa itse asiassa tietuepolymorfismia puhtaasti syntaktisessa muodossa . Toisaalta, jos katsomme kaikki järjestelmän tietueet laajennettavissa oleviksi, niin tietueiden funktiot voidaan kirjoittaa polymorfisiksi.

Esimerkki yksinkertaisimmasta suunnitteluvaihtoehdosta on toteutettu Alice ML :ssä (nykyisten seuraavien ML -sopimusten mukaan ) [36] . Universaalissa kuviossa (ellipsis ) on laajennetut ominaisuudet: sitä voidaan käyttää "rivin kaappaamiseen" tietueen "jäljellä olevan" osan käyttämiseksi arvona:

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

Toiminnallinen päivitys on toteutettu johdannaisena palvelusanan sisältävän rivin kaappaamisesta where. Esimerkiksi seuraava koodi:

> olkoon val r = { a = 1 , c = 3.0 , d = "ei luettelo" , f = [ 1 ], p = [ "ei merkkijono" ], z = EI MITÄÄN } kohdassa { r , jossa d = nolla , p = "hei" } loppu

kirjoitetaan automaattisesti uudelleen muotoon:

> olkoon val r = { a = 1 , c = 3.0 , d = "ei luettelo" , f = [ 1 ], p = [ "ei merkkijono" ], z = EI MITÄÄN } val { d = _, p = _, ... = tmp } = r in { ... = tmp , d = nolla , p = "hei" } loppu

Tietueen ketjutus

Yksi ensimmäisistä ( 1980 -luvun loppu - 1990-luvun alku ) ehdotti erilaisia vaihtoehtoja laajennettavien tietueiden formalisoimiseksi ketjuttamalla ei-polymorfisia tietueita (Harper-Pearce [38] , Wand [39] , Salzmann [40] ). Cardelli käytti jopa ennätysoperaatioita polymorfismin sijaan Amber-kielessä. Ei ole tunnettua tapaa koota näitä laskelmia tehokkaasti; lisäksi nämä laskelmat ovat tyyppiteoreettisen analyysin kannalta erittäin monimutkaisia. [27] [41] [42] [43]

Esimerkiksi [33] :

val auto = { nimi = "Toyota" ; ikä = "vanha" ; id = 6678 } val truck = { nimi = "Toyota" ; id = 19823235 } ... val repaired_truck = { auto ja kuorma }

rivipolymorfismin kirjoittaja ) osoitti, että moninkertaista periytymistä voidaan mallintaa tietueiden ketjutuksella [39] [33] .

Cardellin rakenteelliset alatyypit

Luca Cardelli tutki mahdollisuutta formalisoida " tietuepolymorfismi " tietueiden alatyyppisuhteiden avulla: tätä varten tietuetta käsitellään "universaalina alatyyppinä", toisin sanoen sen arvon annetaan viitata sen supertyyppien koko joukkoon. Tämä lähestymistapa tukee myös menetelmän periytymistä ja toimii tyyppiteoreettisena perustana yleisimmille olio-ohjelmoinnin muodoille . [27] [44] [45]

Cardelli esitteli muunnelman tietuepolymorfismin kokoamismenetelmästä niiden alatyyppien välillä määrittämällä ennalta kaikkien mahdollisten nimikkeiden poikkeama mahdollisesti valtavassa rakenteessa, jossa on monia tyhjiä paikkoja [31] .

Menetelmällä on merkittäviä haittoja. Tyyppijärjestelmän alatyypityksen tuki monimutkaistaa suuresti tyyppiyhdenmukaisuuden tarkistusmekanismia [46] . Lisäksi sen läsnä ollessa lausekkeen staattinen tyyppi lakkaa tarjoamasta täydellistä tietoa merkinnän arvon dynaamisesta rakenteesta . Esimerkiksi kun käytetään vain alatyyppejä, seuraava termi:

> jos tosi , niin { A = 1 , B = tosi } else { B = epätosi , C = "Kissa" } (* val it : {B : bool} *)

on tyyppi {B : bool}, mutta sen dynaaminen arvo on yhtä suuri kuin {A = 1, B = true}, eli tiedot laajennetun tietueen tyypistä katoavat [43] , mikä on vakava ongelma sellaisten toimintojen tarkistamisessa , jotka vaativat täydellistä tietoa arvorakenteesta niiden suorittamiseen (esim. tasa-arvon vertailu ) [19] . Lopuksi, alatyyppien läsnä ollessa tietueiden järjestetyn ja järjestämättömän esityksen välinen valinta vaikuttaa vakavasti suorituskykyyn [47] .

Alatyyppien suosio johtuu siitä, että se tarjoaa yksinkertaisia ja visuaalisia ratkaisuja moniin ongelmiin. Esimerkiksi erityyppiset objektit voidaan sijoittaa yhteen luetteloon, jos niillä on yhteinen supertyyppi [48] .

Wanda rivipolymorfismi

Mitchell Wand ehdotti vuonna 1987 ajatusta(ei nimenomaisesti määritellystä) osasta tietojen keräämisestä sen avulla, jota hän kutsui rivityyppiseksi muuttujaksi ( rivityyppimuuttuja ) [49] .

Rivimuuttuja on tyyppinen muuttuja, joka kulkee kirjoitettujen kenttien (" " parien) äärellisten joukkojen (rivien) läpi (значение : тип). Tuloksena on kyky toteuttaa laaja perintö suoraan ML : n perustana olevan parametrisen polymorfismin päälle mutkistamatta tyyppijärjestelmää alatyyppisäännöillä Tuloksena olevaa polymorfismin tyyppiä kutsutaan rivipolymorfismiksi . Sisäinen polymorfismi ulottuu sekä tyyppien tuloksiin että tyyppien summaan .

Vand lainasi termin englannista. rivi (rivi, ketju, rivi) Algol-68 :sta , jossa se tarkoitti näkemyksiä. Venäjänkielisessä kirjallisuudessa tämä termi Algolin yhteydessä on perinteisesti käännetty "monilajiksi". "Rivimuuttujat" on myös käännetty "merkkijonomuuttujiksi" [41] , mikä voi aiheuttaa sekaannusta merkkijonotyypeissä olevien pienten kirjainten kanssa .

Esimerkki ( OCaml kieli ; postfix syntaksi, record#field) [50] :

# anna send_m a = a # m ;; (* arvo send_m : < m : a; .. > -> a = <hauskaa> *)

Tässä ellipsi (kahdesta pisteestä) on OCamlin hyväksymä syntaksi nimettömälle rivin tyyppiselle muuttujalle . Tällaisen kirjoituksen ansiosta funktiota send_mvoidaan soveltaa minkä tahansa (aiemmin tuntemattoman ) objektityypin objektiin, joka sisältää mvastaavan allekirjoituksen menetelmän.

Alkuperäisen version Wanda-laskennan tyyppivähennys oli epätäydellinen: sarjan laajentamista koskevien rajoitusten puuttumisen vuoksi kentän lisääminen, jos nimet täsmäävät, korvaa nykyisen - tämän seurauksena kaikilla ohjelmilla ei ole päätyyppiä [6] [43] . Tämä järjestelmä oli kuitenkin ensimmäinen konkreettinen ehdotus ML : n laajentamiseksi perintöä tukevilla tietueilla [51] . Seuraavina vuosina ehdotettiin useita erilaisia parannuksia, mukaan lukien ne, jotka tekevät siitä täydellisen [51] [27] .

Merkittävimmän jäljen jätti Didier Remy ( ranska: Didier Rémy ). Hän rakensi käytännöllisen tyyppijärjestelmän, jossa oli laajennettavia tietueita, mukaan lukien täydellinen ja tehokas tyypin rekonstruktioalgoritmi [52] [53] . Remy kerrostaa tyyppien kielen lajikkeiksi muodostaen lajitellun tyyppialgebran ( eng. lajiteltu tyyppialgebra, lajiteltu tyyppien kieli ). Ero tehdään varsinaisten tyyppien (mukaan lukien kenttätyypit) ja kenttätyyppien välillä . niiden väliset kartoitukset otetaan käyttöön ja niiden pohjalta muotoillaan säännöt laajennettujen tietueiden kirjoittamiselle yksinkertaiseksi jatkeeksi klassisille ML - säännöille . Kentän läsnäolotiedot määritellään yhdistämiseksi tyyppilajittelusta kenttälajitteluun . _ _ _ Rivityyppiset muuttujat muotoillaan uudelleen muuttujiksi, jotka kuuluvat kenttälajitteluun ja ovat yhtä suuria kuin poissaolovakio , joka on kenttälajittelun elementti, jolla ei ole vastaavuutta tyyppilajittelussa . Tyypin arviointioperaatio n kentän tietueelle määritellään n-aarisen kentän yhdistämiseksi tyyppiin (jossa jokainen monikko kenttä lasketaan joko läsnäolofunktiolla tai annetaan poissaolovakiolla ).

Yksinkertaistetusti laskennan idea voidaan tulkita tietueen minkä tahansa kentän tyypin laajennukseksi läsnäolo/poissaololipulla ja tietueen esittäminen monikkona , jossa on paikka jokaiselle mahdolliselle kentälle [6] . Toteutusprototyypissä tyyppikielen syntaksi tehtiin lähemmäksi tyyppiteoreettista muotoilua, esimerkiksi [52] :

# anna auton = { nimi = "Toyota" ; ikä = "vanha" ; id = 7866 } ;; (* auto : ∏ (nimi : pre (merkkijono); id : pre (numero); ikä : pre (merkkijono); abs) *) # let truck = { nimi = "Blazer" ; id = 6587867567 } ;; (* kuorma-auto : ∏ (nimi : pre (merkkijono); id : pre (nm); abs) *) # anna henkilö = { nimi = "Tim" ; ikä = 31 ; id = 5656787 } ;; (* henkilö : ∏ (nimi : pre (merkkijono); id : pre (nm); ikä : esi (nm); abs) *)

(symboli ∏Remyssä tarkoittaa tyyppilaskentatoimintoa)

Uuden kentän lisääminen kirjoitetaan konstruktiolla with:

# anna kuljettajan = { henkilö ajoneuvolla = auto } ;; _ (* kuljettaja : ∏ (ajoneuvo : pre (∏ (nimi : pre (merkkijono); id : pre (numero); ikä : pre (merkkijono); abs)); nimi : pre (merkkijono); id : pre (numero)) ; ikä : ennen (nm); abs) *)

Toiminnallinen päivitys kirjoitetaan samalla tavalla, sillä erolla, että jo olemassa olevan kentän mainitseminen ohittaa sen:

# anna truck_driver = { kuljettaja ajoneuvolla = kuorma - auto };; (* kuorma-autonkuljettaja : ∏ (ajoneuvo : pre (∏ (nimi : pre (merkkijono); id : pre (numero); abs)); nimi : pre (merkkijono); id : pre (nm); ikä : pre (numero) ); abs) *)

Tämä järjestely formalisoi tietueiden toimintojen tarkistamiseen ja päätyypin päättelemiseen tarvittavat rajoitukset , mutta se ei johda ilmeiseen ja tehokkaaseen toteutukseen [6] [43] . Remy käyttää tiivistystä, joka on keskimäärin melko tehokasta, mutta lisää ajonaikaista lisäkustannuksia jopa natiivisti monomorfisissa ohjelmissa, ja se sopii huonosti tietueisiin, joissa on monia kenttiä [31] .

Rémy jatkoi tutkimalla sisäisen polymorfismin käyttöä tiedon alatyypityksen yhteydessä korostaen, että nämä ovat ortogonaalisia käsitteitä, ja osoittaen, että tietueet tulevat ilmeikkäimmiksi, kun niitä käytetään yhdessä [54] . Tältä pohjalta hän ehdotti yhdessä Jérôme Vouillonin kanssa kevyttä oliopohjaista laajennusta ML :ään [55] . Tämä laajennus toteutettiin Xavier Leroyn "Caml Special Light" -kielellä muuttaen sen OCamliksi [56] . OCaml - objektimalli on tiiviisti kietoutunut rakenteellisen alatyypityksen ja inline-polymorfismin käyttöön [48] , minkä vuoksi ne joskus tunnistetaan virheellisesti. OCaml - tuotteen sisäinen polymorfismi on tyyppipäätelmän ytimessä ; alatyyppisuhteet eivät ole välttämättömiä tuetussa kielessä, mutta ne lisäävät entisestään joustavuutta käytännössä [55] [50] [48] . OCamlilla on yksinkertaisempi ja kuvaavampi syntaksi tyyppitiedoille.

Jacques Garrigue ( fr. Jacques Garrigue ) toteutti [25] käytännöllisen polymorfisten summien järjestelmän . Hän yhdisti Remin ja Ohorin teoreettisen työn rakentaen keskellä toimivan järjestelmän: tietueen tagien olemassaoloa koskevat tiedot esitetään sukupuolten avulla ja niiden tyypeissä käytetään rivimuuttujia. Jotta kääntäjä voisi erottaa polymorfiset ja monomorfiset summat, Garriga käyttää erityistä syntaksia (backtick, prefix tag). Tämä eliminoi tyyppimäärityksen tarpeen - voit kirjoittaa siihen funktioita välittömästi, ja kääntäjä tulostaa minimiluettelon tunnisteista, kun näitä toimintoja muodostetaan. Tästä järjestelmästä tuli osa OCamlia vuoden 2000 tienoilla , mutta ei monomorfisten summien sijasta , vaan lisäksi , koska ne ovat hieman tehottomampia ja koska jäsennyn täydellisyyttä ei voida hallita , vaikeuttavat virheiden löytämistä (toisin kuin Bloomin ratkaisu ). [25] [57]

Wandin inline-polymorfismin haittoja ovat toteutuksen epäselvyys (ei ole olemassa yhtä systemaattista tapaa kääntää sitä, jokaisella tietyllä rivimuuttujiin perustuvalla tyyppijärjestelmällä on oma toteutus) ja epäselvä suhde teoriaan (ei ole yhtenäistä tyyppitarkastuksen ja päättelyn muotoilu, päättelyn tuki ratkaistiin erikseen ja vaati kokeita erilaisten rajoitusten asettamiseen) [27] .

Läpikuultava Harper-Lilybridge summat

Monimutkaisin tietuetyyppi ovat riippuvaisia tietueita. Tällaiset tietueet voivat sisältää sekä tyyppejä että "tavallisia" arvoja (materialisoituja tyyppejä, reified [9] ), ja tietueen rungossa järjestyksessä seuraavana olevat termit ja tyypit voidaan määrittää niitä edeltävien ehtojen perusteella. . Tällaiset merkinnät vastaavat riippuvaisen tyyppiteorian " heikkoja summia " , jotka tunnetaan myös nimellä " eksistenttiaalit ", ja ne toimivat yleisimpinä perusteluina ohjelmointikielten moduulijärjestelmille [ 58] [59] . Cardelli piti [60] ominaisuuksiltaan samanlaista tyyppiä yhtenä päätyypeistä täysityyppisessä ohjelmoinnissa (mutta kutsui niitä " tupleiksi ").

Robert Harper ja Mark Lillibridge rakensivat [61 ] [59] läpikuultavan summalaskelman perustellakseen muodollisesti korkeamman asteen ensimmäisen luokan moduulikielen , edistyneintunnetun moduulijärjestelmän . Tätä laskelmaa käytetään muun muassa Harper-Stone-semantiikassa , joka edustaa tyyppiteoreettista perustelua Standard ML :lle .

Läpinäkyvät summat yleistävät heikkoja summia otsikoiden ja yhtälöiden avulla, jotka kuvaavat tyyppikonstruktoreja . Termi läpikuultava tarkoittaa , että tietuetyyppi voi sisältää molempia tyyppejä , joilla on eksplisiittisesti viety rakenne, sekä täysin abstrakteja . Sukukerroksella laskennassa on yksinkertainen klassinen koostumus: kaikkien tyyppien sukupuoli ja lajien funktionaaliset suvut erotetaan , tyypitystyyppiset konstruktorit ( ML ei tue polymorfismia korkeammissa suvuissa , kaikki tyyppimuuttujat kuuluvat sukuun , ja tyyppikonstruktorien abstraktio on mahdollista vain funktoreiden kautta [62 ] ). Laskenta tekee eron tietueiden alityypityssäännöt perustyypeinä ja tietuekenttiä niiden osatekijöinä vastaavasti ottaen huomioon "alatyypit" ja "alikentät", kun taas kenttätunnisteiden peittäminen (abstrahointi) on erillinen käsite alatyypeistä. Alatyypitys tässä formalisoi moduulien yhdistämisen liitäntöihin . [61] [9] ${\näyttötyyli \tähti }$ $k_{1}=>k_{2}$ ${\näyttötyyli \tähti }$

Harper-Lilybridge-laskenta on ratkaisematon edes tyyppiyhdenmukaisuuden tarkistuksen kannalta ( Standard ML :ssä ja OCamlissa toteutetut moduulikielen murteet käyttävät tämän laskun rajoitettuja osajoukkoja). Myöhemmin kuitenkin Andreas Rossberg rakensi heidän ideoidensa pohjalta " 1ML "-kielen, jossa perinteiset kielen ydintason tietueet ja moduulitason rakenteet ovat samaa ensiluokkaista konstruktiota [9] (merkittävästi ilmaisuvoimaisempi kuin Cardellin - katso kritiikki ML-moduulikieltä ). Sisällyttämällä Harperin ja Mitchellin [63] kaikkien tyyppien jakamisesta "pienten" ja "suurien" tyyppien universumeihin (yksinkertaistettuna tämä on samanlainen kuin tyyppien perustavanlaatuinen jako yksinkertaisiin ja aggregoituihin tyyppeihin). epäyhtenäiset kirjoitussäännöt), Rossberg tarjosi selvitettävyyden johdonmukaisuustarkistusten lisäksi lähes täydellisen tyyppipäätelmän . Lisäksi 1ML sallii impredikatiivisen polymorfismin [64] . Samanaikaisesti 1ML:n sisäinen kieli perustuu litteään System F ω eikä vaadi riippuvien tyyppien käyttöä metateoriana. Vuodesta 2015 lähtien Rossberg jätti avoimeksi mahdollisuuden lisätä inline polymorfismia 1ML :ään huomauttaen vain, että tämän pitäisi tarjota täydellisempi tyyppipäätelmä [9] . Vuotta myöhemmin hän lisäsi [65] vaikutusten polymorfismin 1 ml:aan .

Ohori-tietueiden polymorfinen laskenta

Atsushi Ohori esitti yhdessä esimiehensä Peter Bunemanin kanssa vuonna 1988 ajatuksen tavallisten tyyppimuuttujien mahdollisten arvojen rajoittamisesta itse tietueiden polymorfisessa tyypittelyssä . Myöhemmin Ohori formalisoi tämän idean merkintäsuvuilla , kun hän oli rakentanut vuoteen 1995 mennessä täysimittaisen laskennan ja menetelmän sen tehokkaaseen laatimiseen [19] [30] . Toteutusprototyyppi luotiin vuonna 1992 SML/NJ [66] -kääntäjän laajennukseksi, jonka jälkeen Ohori johti oman SML# -kääntäjänsä kehittämistä, joka toteuttaa samannimisen Standard ML -murteen . SML# :ssa tietuepolymorfismi toimii perustana SQL - rakenteiden saumaiselle upottamiselle SML - ohjelmiin . Suuret japanilaiset yritykset käyttävät SML# :a ratkaistakseen korkeasti ladattuihin tietokantoihin liittyviä liiketoimintaongelmia [67] . Esimerkki tällaisesta istunnosta ( REPL ) [68] :

hauska varakas { Palkka = s , ... } = s > 100 000 ; (* val wealthy = fn : 'a#{ Palkka:int, ... } -> bool *) hauska nuori x = #Ikä x < 24 ; (* val young = fn : 'a#{ Age:int, ... } -> bool *) hauska nuoriAndRikkakas x = varakas x ja myös nuori x ; (* val youngAndWealthy = fn : 'a#{ Ikä:int, Palkka:int, ... } -> bool *) hauskaa valitse näyttö l pred = fold ( fn ( x , y ) => if pred x then ( näyttö x ) ::y else y ) l nil ; (* val select = fn : ('a -> 'b) -> 'a list -> ('a -> bool) -> 'b list *) hauskaa youngAndWealthyEmployees l = valitse #Nimi l youngAndWealthy ; (* val youngAndWealthyEmployees = fn : 'b#{ Ikä:int, Nimi:'a, Palkka:int, ... } list -> 'a list *)

Ohori kutsui laskentaansa " tietuepolymorfismiksi " ( englanniksi record polymorphism ) tai " polymorphic record calculukseksi " ( englanniksi polymorphic record calculus ), samalla korostaen, että hän, kuten Wand, ei pidä polymorfismia vain tuotetyypeissä , vaan myös tyypeissä . summat [27] .

Ohori-laskennassa on tunnusomaista sukukerroksen intensiivisin käyttö [ 6] . Merkinnässä (viittaustyyppi sukuun ) symboli tarkoittaa joko kaikkien tyyppien sukua ; tai tietuesuku , jolla on muoto , joka tarkoittaa kaikkien tietueiden joukkoa, jotka sisältävät vähintään määritetyt kentät; tai varianttisuku , jonka muoto ilmaisee kaikkien varianttityyppien joukkoa, joka sisältää vähintään määritetyt konstruktorit . Kielen litteässä syntaksissa jonkin merkinnän tyyppirajoitus kirjoitetaan muodossa (katso esimerkit yllä). Ratkaisu on jossain määrin samanlainen kuin Cardelli-Wegnerin [27] rajoitettu kvantifiointi ] . $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#{...}

Ainoa tämän laskun tarjoama polymorfinen operaatio on kentän erotusoperaatio [69] . Ohori oli kuitenkin ensimmäinen, joka esitteli yksinkertaisen ja tehokkaan käännösjärjestelmän tietuepolymorfismille [43] . Hän kutsui sitä "toteutuslaskentaksi" ( toteutuslaskenta ). Tietuetta edustaa vektori, joka on järjestetty leksikografisesti alkuperäisen tietueen kenttien nimien mukaan; kentän osoittaminen nimellä muuttuu kutsuksi välifunktiolle, joka palauttaa tietyn kentän numeron annetussa vektorissa pyydetyllä nimellä ja sen jälkeen vektorin indeksoinnin lasketulla paikkanumerolla. Funktiota kutsutaan vain, kun instantoi polymorfisia termejä, mikä asettaa ajon aikana minimaalisen lisärasituksen polymorfismia käytettäessä, eikä aiheuta lisäkustannuksia monomorfisten tyyppien kanssa työskennellessä. Menetelmä toimii yhtä hyvin mielivaltaisen suurilla merkinnöillä ja muunnelmilla. Laskenta tarjoaa tyyppipäätelmän ja löytää vahvan vastaavuuden teorian kanssa ( yleinen kvantifiointi liittyy suoraan tavanomaiseen vektorin indeksointiin ), ja se on suora jatke Girard-Reynoldsin toisen asteen lambda-laskimelle , joka mahdollistaa useita tunnettuja polymorfisten ominaisuuksien tyypitys siirretään tietueen polymorfismiin [31] .

Käytännössä tukea polymorfisille muunnelmille SML# :ssa ei ole toteutettu, koska se ei ole yhteensopiva Standard ML :n summatyypin määrittelymekanismin kanssa (vaatii summien ja rekursiivisten tyyppien syntaktista erottamista) [70] .

Ohori-laskennan haittana on tietueen laajennus- tai katkaisuoperaatioiden tuen puute [27] [71] [43] .

Ensimmäisen luokan Guster-Jones-pisteet

Hyväksyttyjen tyyppien teoriassa laajennettavat tietueet kuvataan kentän poissaololla ( "puuttuu" predikaatti ) ja kentän ( "on" predikaatti ) läsnäololla . Benedict Gaster ( Benedict R. Gaster ) viimeisteli sen yhdessä teorian kirjoittajan Mark Jonesin ( Mark P. Jones ) kanssa laajennettavien tietueiden osalta implisiittisesti kirjoitettujen kielten käytännölliseksi tyyppijärjestelmäksi, mukaan lukien käännösmenetelmän määrittely [6] . Niissä käytetään termiä ensiluokkaiset tarrat korostaakseen kykyä abstraktisti kenttäoperaatioita staattisesti tunnetuista tarroista. Myöhemmin Gaster puolusti väitöskirjaansa [72] rakennetusta järjestelmästä .

Gaster-Jones-laskenta ei anna täydellistä tyyppipäätelmää . Lisäksi päätettävyysongelmien vuoksi asetettiin keinotekoinen rajoitus: tyhjien sarjojen kielto [73] . Sulzmann yritti muotoilla laskentaa uudelleen [40] , mutta hänen rakentamaansa järjestelmää ei voida laajentaa tukemaan polymorfista tietueen laajennusta, eikä sillä ole universaalia tehokasta käännösmenetelmää [43] .

Daan Leijen lisäsi rivien yhtäläisyyspredikaatin (tai rivien yhtäläisyyspredikaatin ) Gaster-Jones-laskentaan ja siirsi sarjan kielen predikaattien kielelle - tämä varmisti täydellisen tyyppipäätelmän ja poisti tyhjien sarjojen kiellon [74] . Käännettäessä tietueet muunnetaan leksikografisesti järjestetyksi monikkoksi ja käytetään todisteiden käännöstä Gaster-Jones-kaavan mukaisesti. Layenin järjestelmä sallii ilmaisun ilmaisun , kuten korkeamman asteen viestit ( olio-ohjelmoinnin tehokkain muoto ) ja ensimmäisen luokan haarat .

Näiden töiden perusteella on toteutettu laajennuksia Haskell-kieleen [75] .

Gaster-Jonesin tulokset ovat hyvin lähellä Ohorin tuloksia huolimatta merkittävistä eroista tyyppiteoreettisissa perusteluissa, ja suurin etu on tuki ennätyslaajennus- ja katkaisuoperaatioille [6] . Laskennan haittana on, että se perustuu tyyppijärjestelmän ominaisuuksiin , joita ei löydy useimmista ohjelmointikielistä. Lisäksi sen tyyppipäätelmä on vakava ongelma, minkä vuoksi kirjoittajat ovat asettaneet lisärajoituksia. Ja vaikka Layen on poistanut monet puutteet, -haaran käyttäminen ei ole mahdollista. [71]default

Kontrollikonstruktiopolymorfismi

Ohjelmistojärjestelmien kehittymisen myötä summatyypin vaihtoehtojen määrä voi kasvaa , ja kunkin vaihtoehdon lisääminen edellyttää vastaavan haaran lisäämistä jokaiseen tämän tyypin funktioon, vaikka nämä haarat olisivat identtisiä eri funktioissa. Siten toiminnallisuuden lisäämisen monimutkaisuus useimmissa ohjelmointikielissä riippuu epälineaarisesti toimeksiannon ilmoittavista muutoksista. Tämä malli tunnetaan nimellä lausekeongelma . Toinen tunnettu ongelma on poikkeusten käsittely : vuosikymmenien tyyppijärjestelmien tutkimuksen aikana kaikki tyyppiturvallisiksi luokitellut kielet saattoivat silti poistua tekemällä poikkeuksen, koska poikkeuksien kirjoituksesta huolimatta mekanismi nostaa. ja niiden käsittelyä ei kirjoitettu. Vaikka työkaluja poikkeusvirran jäsentämiseen on rakennettu, nämä työkalut ovat aina olleet kielen ulkopuolisia.

Matthias Blume , Andrew Appelin kollega , joka työskentelee projektin seuraajan ML [76] parissa , hänen jatko-opiskelijansa Wonseok Chae ja kollegansa Umut Acar ratkaisivat molemmat ongelmat matemaattisten kaksinaisuuden tulojen ja summien perusteella . Heidän ideoidensa ilmentymä oli kieli MLPolyR [71] [34] [77] , joka perustui Standard ML :n yksinkertaisimpaan osajoukkoon ja täydensi sitä useilla tyyppiturvallisuustasoilla [78] . Wonseok Chai puolusti myöhemmin väitöskirjaansa näistä saavutuksista [78] .

Ratkaisu on seuraava. Duaalisuuden periaatteen mukaan käsitteen johdantomuoto vastaa sen duaalin eliminaatiomuotoa [ 71 ] . Siten summien eliminointimuoto (haarojen analyysi) vastaa merkintöjen johdantomuotoa. Tämä rohkaisee haaroittamiseen saamaan samat ominaisuudet, jotka ovat jo saatavilla merkinnöille – tee niistä ensiluokkaisia objekteja ja salli niiden laajentamisen.

Esimerkiksi yksinkertaisin ilmaisukielen tulkki:

hauska eval e = tapaus e `Const i => i | `Plus (e1,e2) => eval e1 + eval e2

ensiluokkaisen rakentamisen käyttöönoton myötä casesvoidaan kirjoittaa uudelleen seuraavasti:

fun eval e = yhdistä e tapauksiin ` Const i => i | `Plus (e1,e2) => eval e1 + eval e2

jonka casesjälkeen -lohko voidaan hahmontaa:

hauskaa eval_c eval = tapaukset `Const i => i | `Plus (e1,e2) => eval e1 + eval e2 fun eval e = vastaa e kanssa (eval_c eval)

Tämä ratkaisu mahdollistaa default-haaroittamisen (toisin kuin Gaster-Jones-laskennassa ), joka on tärkeä ensiluokkaisten haarojen koostumuksen kannalta [34] . Rivin koostumuksen täydentäminen suoritetaan sanan avulla . nocases

hauska const_c d = tapaukset `Const i => i oletus : d hauska plus_c eval d = tapaukset `Plus (e1,e2) => eval e1 + eval e2 oletus : d fun eval e = täsmää e const_c:n kanssa (plus_c eval nocases ) fun bind env v1 x v2 = jos v1 = v2 niin x else env v2 hauskaa var_c env d = tapaukset `Var v => env v oletus : d hauskaa let_c eval env d = caset ` Let (v,e,b) => eval (bind env v (eval env e)) b oletusarvo : d hauska eval_var env e = vastaa e kanssa const_c (plus_c (eval_var env) (var_c env (let_c eval_var env nocases )))

Kuten näette, uusi koodi, joka on lisättävä järjestelmän laadullisen monimutkaisen kanssa, ei vaadi jo kirjoitetun koodin muuttamista (funktioita const_cja plus_c"ei tiedä mitään" muuttujien ja let-lohkojen tuen lisäämisestä kielen tulkki). Siten ensiluokkaiset laajennettavat tapaukset ovat perustavanlaatuinen ratkaisu lausekeongelmaan , jolloin voidaan puhua laajennettavan ohjelmoinnin paradigmasta [71] [78] . inline polymorfismia , joka on jo tuettu tyyppijärjestelmässä, ja tässä mielessä tällaisen teknisen ratkaisun etuna on sen käsitteellinen yksinkertaisuus [ 34] .

Ohjelmistojärjestelmien laajentaminen edellyttää kuitenkin myös sellaisten poikkeusten käsittelyn hallintaa, jotka voidaan heittää mielivaltaisiin puhelujen sisäkkäisyyksiin. Ja tässä Bloom ja kollegat julistavat uudentyyppisen turvallisuusiskulauseen Milnerin sloganin kehittämisessä : " Typpitarkastuksen läpäisevät ohjelmat eivät aiheuta käsittelemättömiä poikkeuksia ." Ongelmana on, että jos funktiotyypin allekirjoitus sisältää tietoja poikkeuksista, joita tämä funktio voi mahdollisesti aiheuttaa, ja tämän hyväksytyn funktion allekirjoituksen tiedon on oltava tiukasti yhdenmukainen korkeamman asteen funktioparametrin tietojen kanssa (mukaan lukien jos tämä on tyhjä joukko ) - poikkeusten käsittelymekanismin kirjoittaminen vaatii välittömästi itse poikkeustyyppien polymorfismin - muuten korkeamman asteen funktiot lakkaavat olemasta polymorfisia. Samaan aikaan, turvallisella kielellä, poikkeukset ovat laajennettavissa oleva summa [79] [80] [81] , eli varianttityyppi, jonka konstruktorit lisätään ohjelman edetessä. Näin ollen poikkeusvirtaustyyppinen turvallisuus tarkoittaa tarvetta tukea summatyyppejä , jotka ovat sekä laajennettavia että polymorfisia. Tässäkin ratkaisu on rivipolymorfismi .

Kuten Garrigan laskenta , MLPolyR käyttää erityistä syntaksia polymorfisille summille (backtick, johtava tagi), eikä summa-tyypin ennakkoilmoitusta tarvita (eli yllä oleva koodi on koko ohjelma, ei fragmentti). Etuna on, että jäsentämisen täydellisyyden hallinnassa ei ole ongelmaa: MLPolyR:n semantiikka määritellään muuntamalla todistetusti luotettavaksi sisäiseksi kieleksi , joka ei tue summapolymorfismia eikä poikkeuksia (puhumattakaan havaitsemattomista poikkeuksista), joten niiden tarve on käännösaikainen poisto on itsessään todiste luotettavuudesta. [34]

MLPolyR käyttää ei-triviaalia useiden laskelmien ja kaksivaiheisen translaation yhdistelmää. Se käyttää Remy-laskentaa >>> ja tyyppisovitukseen , samalla kun se käyttää kaksinaisuuden periaatetta summien esittämiseen tuloina, kääntäen sitten kielen välimuotoiseksi eksplisiittisesti tyypitetyksi kieleksi polymorfisilla tietueilla ja käyttää sitten Ohorin tehokasta käännösmenetelmää. . Toisin sanoen Ohorin käännösmalli on yleistetty tukemaan Remy-laskentaa [69] . Tyyppiteoreettisella tasolla Bloom esittelee useita uusia syntaktisia merkintöjä kerralla, mikä mahdollistaa sääntöjen kirjoittamisen poikkeuksiin ja ensiluokkaisiin haaroihin. MLPolyR-tyyppinen järjestelmä tarjoaa täyden tyyppipäätelmän , joten kirjoittajat luopuivat litteän syntaksin kehittämisestä eksplisiittisesti kirjoittaville tyypeille ja allekirjoitusten tuesta moduulikielellä .

Leyen -tyyppinen järjestelmä esittelee myös muunnelman haarapolymorfismista: konstruktio voidaan esittää korkeamman asteen funktiona , joka saa merkinnän funktioista, joista jokainen vastaa tiettyä laskentahaaraa ( Haskellin syntaksi sopii tätä muutosta varten, eikä se vaadi tarkistusta). Esimerkiksi: case

dataList a = nolla :: { } | miinukset :: { hd :: a , tl :: Lista a } snoc xs r = tapaus ( käänteinen xs ) r viimeinen xs = snoc xs { nolla = \ r -> _ | _ , miinukset = \ r -> r . hd }

Koska Layenin järjestelmän tietueet ovat laajennettavissa, haaran jäsentäminen on joustavaa dynaamisten päätösten tasolla (kuten ketjutustarkistukset tai assosiatiivisen taulukon käyttäminen ), mutta tarjoaa paljon tehokkaamman toteutuksen (muunnelman nimi vastaa tietueen siirtymää). Oletushaaroitustuki ( default) on kuitenkin jätettävä pois tässä tapauksessa, koska yksi default-pattern vastaisi useita kenttiä (ja siten useita siirtymiä). Leyen kutsuu tätä rakennetta " ensimmäisen luokan kuvioiksi " ( ensimmäisen luokan kuvioiksi ).

Korkeampien sukupuolten polymorfismi

Korkeampilaatuinen polymorfismi tarkoittaa abstraktiota korkeamman asteen tyyppisten konstruktorien eli muodon yli

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

Tämän ominaisuuden tuki vie polymorfismin korkeammalle tasolle tarjoamalla abstraktion sekä tyypeistä että tyyppikonstruktoreista , aivan kuten korkeamman asteen funktiot tarjoavat abstraktiota sekä arvoista että muista funktioista. Korkeampien sukupuolten polymorfismi on luonnollinen osa monissa toiminnallisissa ohjelmointikielissä , mukaan lukien monadit , taitokset ja upotettavat kielet . [62] [82]

Esimerkiksi [62] , jos määrität seuraavan funktion ( Haskell -kieli ):

kun b m = jos b niin m muuten palauttaa ()

sitten sille päätellään seuraava toiminnallinen tyyppi :

milloin :: forall ( m :: * -> * ) . Monadi m => Bool -> m () -> m ()

Allekirjoitus m :: * -> *sanoo, että tyyppimuuttuja m on korkeampaan lajiin kuuluva tyyppimuuttuja ( englanniksi high-kinded type variable ). Tämä tarkoittaa, että se abstraktioi tyyppikonstruktoreista (tässä tapauksessa unary , kuten Maybetai []), joita voidaan soveltaa konkreettisiin tyyppeihin, kuten Inttai (), rakentamaan uusia tyyppejä.

Täystyypin abstraktiota tukevissa kielissä ( Standard ML , OCaml ) kaikkien tyyppimuuttujien on oltava sukua * , muuten tyyppijärjestelmä ei olisi turvallinen . Polymorfismin korkeammissa suvuissa tarjoaa siis itse abstraktiomekanismi yhdistettynä eksplisiittiseen annotaatioon instantiation yhteydessä, mikä on jonkin verran hankalaa. Polymorfismin idiomaattinen toteutus korkeammissa suvuissa on kuitenkin mahdollista ilman erityistä huomautusta - tähän käytetään tyyppitasolla defunktionalisoinnin kaltaista tekniikkaa . [62]

Yleinen polymorfismi

Hyvät järjestelmät varmistavat itse tyyppijärjestelmien turvallisuuden sallimallatyyppiilmaisujen merkityksen hallinnan .

Vaaditaan esimerkiksi toteuttamaan tavanomaisen " vektori "-tyypin (lineaaritaulukko) sijaan tyyppiperhe " pituusvektorin ", eli määrittelemään tyyppi " pituuden mukaan indeksoitu vektori ". Klassinen Haskell -toteutus näyttää tältä [83] :

tiedot Nolla data Succ n data Vec :: * -> * -> * missä Nolla :: Vec a Nolla Miinukset :: a -> Vec a n -> Vec a ( Succ n )

Tässä määritellään ensin fantomityypit [84] eli tyypit, joilla ei ole dynaamista esitystapaa. Rakentajat Zero ja Succtoimivat "tyyppikerrosarvoina", ja muuttuja npakottaa rakentajan rakentamien eri betonityyppien epätasa-arvon Succ. Tyyppi Vecmääritellään yleistetyksi algebralliseksi tietotyypiksi (GADT).

Ratkaisu olettaa ehdollisesti, että phantom-tyyppiä nkäytetään vektorin kokonaislukuparametrin mallintamiseen Peanon aksioomien pohjalta - eli rakennetaan vain lausekkeita, kuten Succ Zero, Succ Succ Zerojne Succ Succ Succ Zero. Vaikka määritelmät on kirjoitettu tyyppikielellä , ne itse on muotoiltu kirjoittamattomalla tavalla. Tämä näkyy allekirjoituksesta Vec :: * -> * -> *, mikä tarkoittaa, että parametreina annetut betonityypit kuuluvat sukuun * , mikä tarkoittaa, että ne voivat olla mitä tahansa betonityyppiä. Toisin sanoen merkityksettömät tyyppiset ilmaukset, kuten Succ Booltai eivät ole kiellettyjä täällä Vec Zero Int. [83]

Edistyneempi laskutoimitus mahdollistaisi tyyppiparametrin alueen määrittämisen tarkemmin:

data Nat = nolla | Succ Nat data Vec :: * -> Nat -> * missä VNil :: Vec a Zero VCons :: a -> Vec a n -> Vec a ( Succ n )

Mutta yleensä vain pitkälle erikoistuneilla järjestelmillä, joissa on riippuvaisia tyyppejä [85] , jotka on toteutettu sellaisilla kielillä kuin Agda , Coq ja muut, on tällainen ilmaisukyky. Esimerkiksi agdan kielen näkökulmasta merkintä Vec :: * -> Nat -> *tarkoittaisi, että tyypin sukupuoli Vec riippuu tyypistä Nat(eli yhden lajin elementti riippuu toisen, alemman lajin elementistä ).

Vuonna 2012 Haskell -kieleen rakennettiin laajennus [83] , joka toteuttaa edistyneemmän sukupuolijärjestelmän ja tekee yllä olevasta koodista oikean Haskell-koodin. Ratkaisu on, että kaikki tyypit (tietyin rajoituksin) " ylennetään " automaattisesti ( eng. promote ) korkeammalle tasolle, jolloin muodostuu samannimiset suvut, joita voidaan käyttää eksplisiittisesti. Tästä näkökulmasta merkintä ei ole riippuvainen - se tarkoittaa vain, että vektorin toisen parametrin on kuuluttava nimettyyn sukuun , ja tässä tapauksessa tämän suvun ainoa elementti on samanniminen tyyppi. Vec :: * -> Nat -> *Nat

Ratkaisu on melko yksinkertainen sekä kääntäjässä toteutuksen että käytännön saavutettavuuden kannalta. Ja koska tyyppipolymorfismi on luonnostaan Haskellin semantiikan luonnollinen elementti , tyypin edistäminen johtaa lajipolymorfismiin , mikä sekä lisää koodin uudelleenkäyttöä että tarjoaa korkeamman tyyppiturvallisuuden tason . Esimerkiksi seuraavaa GADT :tä käytetään tyypin tasa-arvon tarkistamiseen:

tiedot EqReﬂ a b missä Reﬂ :: EqReﬂ a a

on klassisen Haskellin sukupuoli * -> * -> *, mikä estää sen käyttämisen testaamaan tyyppikonstruktoreiden , kuten Maybe. Tyypin edistämiseen perustuva sukujärjestelmä päättelee polymorfisen suvun forall X. X -> X -> *, mikä tekee tyypistä EqReﬂyleisemmän. Tämä voidaan kirjoittaa suoraan:

data EqReﬂ ( a :: X ) ( b :: X ) missä Reﬂ :: kaikille X . kaikille ( a :: X ) . EqReﬂ a a

Vaikutuspolymorfismi

Gifford ja Lucassen ehdottivat tehostejärjestelmiä 1980-luvun toisella puoliskolla [86] [87] [88] tavoitteenaan eristää sivuvaikutukset kilpailullisen ohjelmoinnin turvallisuuden ja tehokkuudentarkempaan hallintaan.

Tässä tapauksessa efektipolymorfismi tarkoittaa tietyn funktion puhtauden kvantifiointia , eli lipun sisällyttämistä funktionaaliseen tyyppiin , joka luonnehtii funktiota puhtaaksi tai epäpuhtaiseksi . Tämä kirjoituslaajennus mahdollistaa korkeamman asteen funktioiden puhtauden erottamisen niille argumentteina välitettyjen funktioiden puhtaudesta.

Tämä on erityisen tärkeää siirryttäessä funktioihin moduulien ( abstrakteja tyyppejä sisältävät tietueet ) - funktionaaleihin -, koska puhtausolosuhteissa niillä on oikeus olla aplikatiivisia, mutta sivuvaikutusten esiintyessä niiden on generoitava tyyppiturvallisuuden varmistamiseksi . (katso tästä lisää ML-moduulin kielen tyyppien vastaavuudesta ). Siten korkeamman asteen ensimmäisen luokan moduulien kielessä efektipolymorfismi osoittautuu välttämättömäksi perustaksi generatiivisuuden polymorfismin tukemiselle : puhtauslipun välittäminen funktorille tarjoaa valinnan aplikatiivisen ja generatiivisen semantiikan välillä yhdessä järjestelmässä. [65]

Ohjelmointikielien tuki

Tyyppiturvallinen parametrinen polymorfismi on saatavilla Hindley-Milner -tyyppisillä kielillä — myös ML - murteilla ( Standard ML , OCaml , Alice , F# ) ja niiden jälkeläisillä ( Haskell , Clean , Idris , Mercury , Agda ) kuten niiltä perityissä hybridikielissä ( Scala , Nemerle ).

Yleiset tietotyypit (geneerit) eroavat parametrisesti polymorfisista järjestelmistä siinä, että ne käyttävät rajoitettua kvantifiointia , joten niiden arvo ei voi olla korkeampi kuin 1 . Ne ovat saatavilla kielillä Ada , Eiffel , Java , C# , D , Rust ; ja myös Delphissä vuoden 2009 versiosta lähtien. Ne ilmestyivät ensimmäisen kerran CLU :ssa .

Intensionaalinen polymorfismi

Intensionaalinen polymorfismi on tekniikka parametrisen polymorfismin kokoamisen optimoimiseksi, joka perustuu monimutkaiseentyyppiteoreettiseen analyysiin , joka koostuu tyyppien laskemisesta ajon aikana. Intensionaalinen polymorfismi mahdollistaa tunnisteettoman roskien keräämisen ,argumenttien siirtämisen laatikoitta funktioille ja laatikoidut (muistioptimoidut) litteät tietorakenteet. [89] [90] [91]

Monomorfisaatio

Monomorfisointi on tekniikka parametrisen polymorfismin kokoamisen optimoimiseksi ,joka koostuu monomorfisen ilmentymän generoimisesta jokaista polymorfisen funktion tai tyypin käyttötapausta varten . Toisin sanoen parametrinen polymorfismi lähdekooditasolla tarkoittaa ad hoc -polymorfismia kohdealustan tasolla. Monomorfisointi parantaa suorituskykyä (tarkemmin sanottuna tekee polymorfismista "vapaaksi"), mutta samalla se voi suurentaa tulostettavan konekoodin kokoa . [92]

Hindley - Milner

Klassisessa versiossa ML -kielen taustalla oleva Hindley-Milner-tyyppinen järjestelmä (myös yksinkertaisesti "Hindley-Milner" tai "X-M", englanniksi HM ) [93] [94] on järjestelmän F osajoukko , jota rajoittaa predikatiivi prenex polymorfismi mahdollistaa automaattisen tyyppipäätelmän , jolle Hindley-Milner on perinteisesti sisällyttänyt myös Robin Milnerin kehittämän ns. " Algorithm W " .

Monet X-M:n toteutukset ovat järjestelmän parannettuja versioita, jotka edustavat " päätyyppistä tyyppiä " [93] [2] , joka yhdellä kertaa lähes lineaarisella monimutkaisuudella päättelee samanaikaisesti kunkin lausekkeen yleisimmät polymorfiset tyypit ja tarkastaa niiden tiukasti . sopimus .

Hindley-Milner-tyyppistä järjestelmää on sen perustamisesta lähtien laajennettu useilla tavoilla [95] . Yksi tunnetuimmista laajennuksista on tuki ad-hoc-polymorfismille tyyppiluokkien kautta , jotka yleistetään edelleen hyväksytyiksi -tyypeiksi .

Automaattinen tyyppipäätelmä pidettiin välttämättömänä ML : n alkuperäisessä kehittämisessä interaktiivisena lauseentodistusjärjestelmänä " Logic for Computable Functions ", minkä vuoksi vastaavat rajoitukset asetettiin. Myöhemmin ML :n perusteella kehitettiin joukko tehokkaasti käännettyjä yleiskäyttöisiä kieliä, jotka on suunnattu laajamittaiseen ohjelmointiin , ja tässä tapauksessa tyyppipäätelmän tukemisen tarve vähenee jyrkästi, koska moduulirajapinnat teollisessa käytännössä on joka tapauksessa nimenomaisesti merkittävä tyypit [81 ] . Tästä syystä on ehdotettu monia Hindley-Milner-laajennuksia, jotka välttävät tyyppipäätelmät voimaantumisen hyväksi, jopa täydellisen System F :n tuen, jossa on impredikatiivista >>> , kuten korkeamman asteen moduulikielelle , joka alun perin perustui eksplisiittinen moduulityyppinen huomautus ja siinä on monia laajennuksia ja murteita sekä Haskell-kielilaajennuksia ( , ja ). Rank2TypesRankNTypesImpredicativeTypes

Standardi- ML :n MLton- kääntäjä monomorfoi , mutta muiden Standard ML :ään sovellettavien optimointien vuoksi tuloskoodin lisäys ei ylitä 30 % [92] .

C ja C++

C:ssä funktiot eivät ole ensiluokkaisia objekteja , mutta on mahdollista määritellä funktioosoittimia , joiden avulla voidaan rakentaa korkeamman asteen funktioita [96] . Vaarallinen parametrinen polymorfismi on myös saatavilla antamalla tyypin vaaditut ominaisuudet eksplisiittisesti tyypittämättömän osoittimen edustaman kielen tyypittämättömän osajoukon kautta [ Taaksepäin.)"osoittimeksiyleiseksi(kutsutaan kieliyhteisössä "void*97] ad-hoc-polymorfismia , koska se ei muuta osoittimen esitystapaa, se on kuitenkin kirjoitettu eksplisiittisesti ohittamaan kääntäjän tyyppijärjestelmä [96] . void*

Esimerkiksi vakiofunktio qsortpystyy käsittelemään minkä tahansa tyyppisiä elementtejä, joille on määritelty vertailufunktio [96] .

struct segment { int aloitus ; int end ; }; int seg_cmpr ( struct segment * a , struct segment * b ) { return abs ( a -> loppu - a -> alku ) - abs ( b -> loppu - b -> alku ); } int str_cmpr ( merkki ** a , merkki ** b ) { return strcmp ( * a , * b ); } struct segmentti segs [] = { { 2 , 5 }, { 4 , 3 }, { 9 , 3 }, { 6 , 8 } }; char * strs [] = { "kolme" , "yksi" , "kaksi" , "viisi" , "neljä" }; tärkein () { 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:ssä on kuitenkin mahdollista toistaa idiomaattisesti tyypitetty parametrinen polymorfismi ilman void*[98] .

C++-kieli tarjoaa mallialijärjestelmän , joka näyttää parametripolymorfismalta, mutta on semanttisesti toteutettu yhdistelmällä ad hoc -mekanismeja:

malli < tyypin nimi T > T max ( T x , T y ) { jos ( x < y ) paluu y ; muu paluu x ; } int main () { int a = max ( 10 , 15 ); kaksinkertainen f = max ( 123,11 , 123,12 ); ... }

: n monomorfoiminen C++-malleja käännettäessä on väistämätöntä , koska kielen tyyppijärjestelmästä puuttuu tuki polymorfismille - polymorfinen kieli on tässä staattinen lisäosa monomorfisen kielen ytimeen [99] . Tämä johtaa moninkertaiseen kasvuun vastaanotetun konekoodin määrässä , joka tunnetaan nimellä " koodin paisuminen " [100] .

Historia

Parametrisen polymorfismin merkinnän lambda -laskennan kehityksenä (kutsutaan polymorfiseksi lambda-laskuksi tai järjestelmäksi F ) kuvasi muodollisesti loogikko Jean-Yves Girard [101] [102] ( 1971 ), hänestä riippumatta samanlainen. järjestelmän kuvasi tietojenkäsittelytieteilijä John S. Reynolds [103] ( 1974 ) [104] .

Parametrinen polymorfismi esiteltiin ensimmäisen kerran ML :ssä vuonna 1973 [41] [105] . Hänestä riippumatta parametriset tyypit toteutettiin Barbara Liskovin johdolla CLU :ssa ( 1974 ) [41] .

Katso myös

Tyyppi rakentaja
Suku (tyyppiteoria)
Polymorfinen rekursio

Muistiinpanot

↑ 1 2 Strachey, "Fundamental Concepts", 1967 .
↑ 1 2 Pierce, 2002 .
↑ Cardelli, Wegner, "Tyyppien ymmärtämisestä", 1985 , 1.3. Polymorfismin tyypit, s. 6.
↑ 1 2 Appel, "Critique of SML", 1992 .
↑ 1 2 Jones, "Theory of Qualified Types", 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. Thesis), 2009 , s. 91-92.
↑ 1 2 3 4 5 6 Rossberg, "1ML - Core and Modules United (F-ing First-class Modules)", 2015 .
↑ Blume, "Poikkeuskäsittelijät", 2008 , s. yksitoista.
↑ Wells, 1994 .
↑ Pierce, 2002 , 22 Tyyppien rekonstruktio, s. 361.
↑ Pierce, 2002 , 23.6 Pyyhkiminen, tyypitys ja tyypin rekonstruktio, s. 378-381.
↑ Remy, "ML abstrakteilla ja tietuetyypeillä", 1994 .
↑ Garrigue, Remy, "Semi-Explicit First-Class Polymorphism for ML", 1997 .
↑ Reynolds, "Ohjelmointikielten teoriat", 1998 , 17. Polymorfismi. Bibliografiset huomautukset, s. 393.
↑ Ensiluokkainen polymorfismi MLtonissa . Haettu 28. heinäkuuta 2016. Arkistoitu alkuperäisestä 28. marraskuuta 2015. (määrätön)
↑ Pierce, 2002 , 22.7 Polymorphism via let, s. 354-359.
↑ 1 2 3 4 5 Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 .
↑ Dushkin, "Monomorfismi, polymorfismi ja eksistentiaaliset tyypit", 2010 .
↑ Cardelli, "Tyypillinen ohjelmointi", 1991 , s. kaksikymmentä.
↑ Pierce, 2002 , 23.10 Impredikatiivisuus, s. 385.
↑ Pierce, 2002 , luku 22. Type Reconstruction. Kohta 22.8. Lisähuomautuksia, s. 361-362.
↑ Wonseok Chae (Ph.D. Thesis), 2009 , s. neljätoista.
↑ 1 2 3 Garrigue, "Polymorphic Variants", 1998 .
↑ Blume, "Extensible Programming with First Class Cases", 2006 , s. kymmenen.
↑ 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, s. 3-6.
↑ Leijen, "First-class Labels", 2004 , s. yksi.
↑ Gaster, Jones, "Polymorphic Extensible Records and Variants", 1996 , Abstract, s. yksi.
↑ 1 2 Paulson, "ML for the Working Programmer", 1996 , 2.9 Records, s. 35.
↑ 1 2 3 4 Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , 1.2 Compilation Method for Record Polymorphism, s. 6-8.
↑ Harper, "Intro to SML", 1986 .
↑ 1 2 3 Remy, "Type Inference for Records", 1991 , s. 2.
↑ 1 2 3 4 5 Blume, "Rivipolymorfismi työssä", 2007 .
↑ Toiminnallisen tietueen päivitys . Haettu 30. kesäkuuta 2016. Arkistoitu alkuperäisestä 2. kesäkuuta 2016. (määrätön)
↑ 1 2 Alice ML:n syntaktisia parannuksia . Haettu 30. kesäkuuta 2016. Arkistoitu alkuperäisestä 27. marraskuuta 2016. (määrätön)
↑ Toiminnallinen tietueen laajennus ja rivien sieppaus . Haettu 30. kesäkuuta 2016. Arkistoitu alkuperäisestä 13. elokuuta 2016. (määrätön)
↑ Harper, Pierce, "Record calculus based on symmetric concatenation", 1991 .
↑ 1 2 Wand, "Tyyppipäätelmä tietueiden ketjuttamiseen ja moninkertaiseen periytymiseen", 1991 .
↑ 12 Sulzmann , 1997 .
↑ 1 2 3 4 Pierce, 2002 , 1.4 Lyhyt historia, s. 11-13.
↑ Remy, "Type Inference for Records", 1991 , s. 2-3.
↑ 1 2 3 4 5 6 7 Leijen, "First-class Labels", 2004 , s. 13-14.
↑ Cardelli, "Multiperinnön semantiikka", 1988 .
↑ Cardelli, Wegner, "Tyyppien ymmärtämisestä", 1985 .
↑ Pierce, 2002 , 16. Alatyypin metateoria, s. 225.
↑ Pierce, 2002 , 11.8 Nauhoitukset, s. 135.
↑ 1 2 3 Minsky kääntänyt DMK, 2014 , Alatyypitys ja tekstin sisäinen polymorfismi, s. 267-268.
↑ Wand, "Tyyppipäätelmä esineille", 1987 .
↑ 1 2 Minsky kääntänyt DMK, 2014 , Object Polymorphism, s. 255-257.
↑ 1 2 Remy, "Type Inference for Records", 1991 , Aiheeseen liittyvä teos, s. 3.
↑ 1 2 Remy, "Type Inference for Records", 1991 .
↑ Blume, "Extensible Programming with First Class Cases", 2006 , s. yksitoista.
↑ Remy, "Alatyypit ja rivipolymorfismi", 1995 .
↑ 1 2 Remy, Vouillon, "Objective ML", 1998 .
↑ Pierce, 2002 , 15.8 Lisähuomautuksia, s. 223.
↑ Minsky kääntänyt DMK, 2014 , Polymorfiset variantit, s. 149-158.
↑ Pierce, 2002 , 24 Eksistentiaaliset tyypit, s. 404.
↑ 1 2 Reynolds, "Ohjelmointikielten teoriat", 1998 , 18. Moduulimääritykset, s. 401-410.
↑ Cardelli, "Tyypillinen ohjelmointi", 1991 , 4.4. Tuple-tyypit, s. 20-23.
↑ 1 2 Harper, Lillibridge, "Type-Theoretic Approach to Higher-Order Modules with Sharing", 1993 .
↑ 1 2 3 4 Yallop, valkoinen, "Kevyt korkealaatuinen polymorfismi", 2014 .
↑ Harper, Mitchell, "SML:n tyyppirakenne", 1993 .
↑ Rossberg, "1ML - Core and Modules United (F-ing First-class Modules)", 2015 , Impredicativity Reloaded, s. 6.
↑ 1 2 Rossberg, "1ML erikoistehosteilla (F-ing Generativity Polymorphism)", 2016 .
↑ Ohori, "Compilation Method for Polymorphic Record Calculi", 1992 .
↑ Ohori - SML# (esitys) (downlink) . Haettu 30. kesäkuuta 2016. Arkistoitu alkuperäisestä 27. elokuuta 2016. (määrätön)
↑ Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , s. 38.
↑ 1 2 Blume, "Extensible Programming with First Class Cases", 2006 , s. 9.
↑ Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , 5 Implementaion, s. 37.
↑ 1 2 3 4 5 Blume, "Extensible Programming with First-Class Cases", 2006 .
↑ Gaster (Ph.D. Thesis), 1998 .
↑ Leijen, "First-class Labels", 2004 , s. 7.
↑ Leijen, "First-class Labels", 2004 .
↑ Laajennettavat tietueet Haskell-Wikissä (downlink)
↑ Blumen henkilökohtainen sivu . Haettu 30. kesäkuuta 2016. Arkistoitu alkuperäisestä 19. toukokuuta 2016. (määrätön)
↑ Blume, "Poikkeuskäsittelijät", 2008 .
↑ 1 2 3 Wonseok Chae (Ph.D. Thesis), 2009 .
↑ Paulson, "ML for the Working Programmer", 1996 , 4.6 Poikkeusten ilmoittaminen, s. 135.
↑ Harper, "Practical Foundations for Programming Languages", 2012 , 28.3 Poikkeustyyppi, s. 258-260.
↑ 1 2 ML2000 Preliminary Design, 1999 .
↑ Harper, "Practical Foundations for Programming Languages", 2012 , luku 22. Rakentajat ja lajit, s. 193.
↑ 1 2 3 Weirich et al, "Giving Haskell a Promotion", 2012 .
↑ Fluet, Pucella, "Phantom Types and Subtyping", 2006 .
↑ Pierce, 2002 , 30.5 Jatketaan eteenpäin: Riippuvaiset tyypit, s. 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 Polymorfismin lajikkeet, s. 364-365.
↑ 1 2 viikkoa, "Whole-Program Compilation in MLton", 2006 .
↑ 1 2 Hindley, "Principal Type Scheme", 1969 .
↑ Milner, "Tyyppipolymorfismin teoria", 1978 .
↑ Jones, "FP with Overloading and HO Polymorphism", 1995 .
↑ 1 2 3 Kernighan B. , Ritchie D. C-ohjelmointikieli = C-ohjelmointikieli. - 2. painos - Williams , 2007. - S. 304. - ISBN 0-13-110362-8 . , Luku 5.11. Toimintoosoittimet
↑ Appel, "SML:n kritiikki", 1992 , s. 5.
↑ Oleg Kiseljov. Todella polymorfiset luettelot C:ssä . okmij.org. Haettu 22. marraskuuta 2016. Arkistoitu alkuperäisestä 30. tammikuuta 2017. (määrätön)
↑ Mitchell, "Concepts in Programming Languages", 2004 , 6.4. Polymorfismi ja ylikuormitus, s. 145-151.
↑ Scott Meyers . Koodin turvotus mallien takia . comp.lang.c++.moderated . Usenet (16. toukokuuta 2002). Haettu: 19. tammikuuta 2010. (määrätön)
↑ Girard, "Extension of Type Theory", 1971 .
↑ Girard, "Higher-order calculus", 1972 .
↑ Reynolds, "Theory of Type Structure", 1974 .
↑ Pierce, 2002 , 23.3 System F, s. 365-366.
↑ Milner et ai, "LCF", 1975 .

Kirjallisuus

Christopher Strachey. Ohjelmointikielten peruskäsitteet . - 1967. Arkistoitu 12. elokuuta 2017.
- Uudelleenjulkaistu: Christopher Strachey. Ohjelmointikielten peruskäsitteet // Korkeamman asteen ja symbolinen laskenta . - 2000. - T. 13 . - S. 11-49 . - doi : 10.1023/A:1010000313106 .

J Roger Hindley. Objektin päätyyppikaavio kombinatorisessa logiikassa // Transactions of the American Mathematical Society . - American Mathematical Society, 1969. - Voi. 146 . - s. 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 (ranska) // Proceedings of the Second Scandinavian Logic Symposium. - Amsterdam, 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 (ranska) . — Université Paris 7, 1972.

John C. Reynolds. Kohti tyyppirakenteen teoriaa // Tietojenkäsittelytieteen luentomuistiinpanot . - Paris: Colloque sur la programmation, 1974. - Vol. 19 . - S. 408-425 . - doi : 10.1007/3-540-06859-7_148 .

Milner R. , Morris L., Newey M. Laskettavien funktioiden logiikka refleksiivisillä ja polymorfisilla tyypeillä // Arc-et-Senans. — Pros. Konferenssi ohjelmien testaamisesta ja parantamisesta, 1975.

Robin Milner . Ohjelmoinnin tyyppipolymorfismin teoria. - 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 // Matemaattiset rakenteet tietojenkäsittelytieteessä. - 1991. -1,numero. 1.

Luca Cardelli , Peter Wegner. Tyyppien, tietojen abstraktion ja polymorfismin ymmärtämisestä //ACM Computing Surveys. - New York, USA:ACM, 1985. -17,no. 4. -S. 471-523. —ISSN 0360-0300. -doi:10.1145/6041.6042.

Robert Harper . Standard ML:n esittely. - Carnegie Mellon University, 1986. - 97 s. — ISBN PA 15213-3891. (Venäjän kieli)

John M. Lucassen, David K. Gifford. Toiminnallisen ja pakottavan ohjelmoinnin integrointi . – 1986.

Luca Cardelli . Polymorfinen perustyyppitarkistus. – 1987.

Mitchell Wand . Täydellinen tyyppipäätelmä yksinkertaisille objekteille // In Proc. Toinen IEEE-symposiumi logiikasta tietojenkäsittelytieteessä. - 1987. -s. 37-44.

Martín Abadi, Luca Cardelli , Pierre-Louis Curien. Muodollinen parametrinen polymorfismi . – POPL, 1993.

Luca Cardelli . Moniperinnön semantiikka // Inf. Comput. 76. - 1988. -P. 138-164.

John M. Lucassen, David K. Gifford. Polymorfiset tehostejärjestelmät . – 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 . Tyypillinen ohjelmointi // IFIP State-of-the-Art -raportit. - New York: Springer-Verlag, 1991. -Iss. Ohjelmointikäsitteiden muodollinen kuvaus. -s. 431-507.

Robert Harper , Benjamin Pierce. Kirjaa symmetriseen ketjutukseen perustuva laskenta // CMU-CS-90-157R. - Carnegie Mellon University, Naval Researchin tukema ja valvoma, 1991.

Mitchell Wand . Tyyppipäätelmä tietueiden ketjuttamista ja moninkertaista periytymistä varten // Valintoja vuoden 1989 IEEE Symposium on Logic in Computer Science -symposiumista. - Information and Computation, 1991. -T. 93,no. 1. -doi:10.1016/0890-5401(91)90050-C.

Andrew W. Appel. Standard ML:n kritiikki . - Princetonin yliopisto, 1992.

Mark P. Jones. Hyväksyttyjen tyyppien teoria . — ESOP , Springer-Verlag Lecture Notes in Computer Science, 1992.

Atsushi Ohori. Kokoonpanomenetelmä ML-tyyliselle polymorfiselle tietuelaskulle // POPL: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages,. - Kioton yliopisto, ACM , 1992. - S. 154-165 . - doi : 10.1.1.105.7655 .

J.P. Talpin, P. Jouvelot. Polymorfinen tyyppi, alue ja vaikutus // 2(3):245271. – JFP , 1992.

Robert Harper , John C. Mitchell. Standardi-ML:n tyyppirakenteesta. -ACMTOPLAS, 1993. -S. 211-252.

Robert Harper , Mark Lillibridge. Tyyppiteoreettinen lähestymistapa korkeamman asteen moduuleihinjakamalla . -ACMPress,POPL, 1993. - ISBN CMU-CS-93-197. -doi:10.1.1.14.3595.

Didier Remy. Objektien ohjelmointi ML-ART:lla: ML:n laajennus abstrakteilla ja tietuetyypeillä . - International Symposium on Theoretical Aspects of Computer Software, Springer-Verlag, 1994. - S. 321-346 .

JB Wells. Typability ja tyyppitarkistus toisen asteen lambda-laskennassa ovat samanarvoisia ja ratkaisemattomia // Proceedings of 9th Annual IEEE . - Symposium on Logic in Computer Science (LIS), 1994. - S. 176-185 .

Robert Harper , . Polymorfismin laatiminen Intensionaalisen tyyppianalyysin avulla. – 1995.

Atsushi Ohori. Polymorfinen tietuelaskenta ja sen kokoaminen . - Kioton yliopisto, ACM , 1995. - S. 844-895 .

Mark P. Jones. Funktionaalinen ohjelmointi ylikuormituksen ja korkeamman asteen polymorfismin kanssa . - Springer-Verlag Lecture Notes, 1995. - doi : 10.1.1.26.9460 .

Didier Remy. Paremmat alatyypit ja rivimuuttujat tietuetyypeille // Esitetty Newton Instituten tietotekniikan tyyppien edistymistä käsittelevässä työpajassa. - Cambridge, Iso-Britannia, 1995.

Lawrence C. Paulson . ML työohjelmoijalle. – 2. - Cambridge, Iso-Britannia: Cambridge University Press, 1996. - 492 s. -ISBN 0-521-57050-6(kovakantinen), 0-521-56543-X (nidottu).

Benedict R. Gaster, Mark P. Jones. Polymorfinen tyyppijärjestelmä laajennettaville tietueille ja vaihtoehdoille // Tekninen raportti NOTTCS-TR-96-3. – Nottinghamin yliopisto, 1996.

Jacques Garrigue, Didier Remy. Puolieksplisiittinen ensimmäisen luokan polymorfismi ML:lle // Academic Press. — Information and Computation, 1997.

M. Sulzmann. Recording Systems // Tekninen raportti YALEU/DCS/RR-1128. - Yalen yliopisto, 1997. - doi : 10.1.1.17.6563 .

Karl Crary, Stephanie Weirich, J. Gregory Morrisett. Intensionaalinen polymorfismi tyypinpoistosemantiikassa . — ICFP , 1998.

Benedict R. Gaster. Tietueet, muunnelmat ja hyväksytyt tyypit // Tekninen raportti NOTTCS-TR-98-3. — Ph.D. Väitöskirja, 1998.

Jacques Garrigue. Ohjelmointi polymorfisilla vaihtoehdoilla . - Kioton yliopisto, 1998.

Didier Rémy, Jérome Vouillon. Objective ML: Tehokas olio-laajennus ML:lle . - Theory and Practice of Object Systems, ACM , 1998. - V. 4 (1) . - S. 27-50 .

John C. Reynolds. Ohjelmointikielten teoriat . - Cambridge University Press, 1998. - ISBN 978-0-521-59414-1 (kovakantinen), 978-0-521-10697-9 (nidottu).

ML2000-työryhmä. ML2000 :n periaatteet ja alustava suunnittelu . – 1999.

Benjamin Pierce. Tyypit ja ohjelmointikielet . - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Käännös venäjäksi: Benjamin Pierce. Tyypit ohjelmointikielillä. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .

John C. Mitchell Ohjelmointikielten käsitteet. - Cambridge University Press, 2004. - ISBN 0-511-04091-1 (eBook in netLibrary); 0-521-78098-5 (kovakantinen).

Jens Palsberg, Tian Zhao. Tyyppipäätelmä tietueiden ketjutusta ja alatyypitystä varten . - 2004. Arkistoitu 16. syyskuuta 2016.

Daan Leijen. Ensiluokkaiset tarrat laajennetuille riveille // TechReport UU-CS-2004-51. - Utrechtin yliopisto, 2004.

Matthias Blume, Umut A. Acar, Wonseok Chae. Laajennettava ohjelmointi ensiluokkaisilla koteloilla . – ICFP , 2006.

Matthew Fluet, Riccardo Pucella. Haamutyypit ja alatyypit . – JFP , 2006.

Stephen Weeks. Koko ohjelman kokoelma MLtonissa . - 2006. Arkistoitu 29. kesäkuuta 2007.

Matthias Blume. Tietueet, summat, tapaukset ja poikkeukset: Rivipolymorfismi työssä : puhevideo. - Microsoft, 2007.

Matthias Blume, Umut A. Acar, Wonseok Chae. Poikkeuskäsittelijät laajennettavissa olevina koteloina . - Toyota Technological Institute Chicagossa, APLAS, 2008.

Wonseok Chae. Tyyppi Safe Extensible Programming // Ph.D. opinnäytetyö. – Toyota Technological Institute Chicagossa, 2009.

Roman Dushkin. Monomorfismi, polymorfismi ja eksistentiaaliset tyypit . – 2010.

Jeremy Yallop, Leo White. Kevyt korkealaatuinen polymorfismi . — International Symposium on Functional and Logic Programming, 2014.

Robert Harper . Ohjelmointikielten käytännön perusteet. - versio 1.37 (tarkistettu 11.1.2014). - lisensoitu Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License -lisenssillä., 2012. - 544 s. Arkistoitu24. lokakuuta 2015Wayback Machinessa

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

Minsky, Madhavapeddy, Hickey. Real World OCaml: Funktionaalinen ohjelmointi massoille . - O'Reilly Media, 2013. - 510 s. — ISBN 9781449324766 .
- Käännös venäjäksi:
  Minsky, Madhavapeddy, Hickey. Ohjelmointi OCaml-kielellä . - DMK, 2014. - 536 s. - ISBN 978-5-97060-102-0 . (Venäjän kieli)

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

Andreas Rossberg. 1 ml erikoistehosteilla (F-ing Generativity Polymorphism) . – WadlerFest, Google, 2016.

Haskell-Wiki: Eksistentiaaliset tyypit . (määrätön)

Haskell-Wiki: Rank-N tyypit . (määrätön)

Haskell-Wiki: Impredikatiiviset tyypit . (määrätön)

Jacques Garrigue. OCaml-opas: Polymorfiset variantit . (määrätön)

Tietotyypit
Käsittämätön	Bitti Napostella Tavu qubit Kohdella Piirre Sana
Numeerinen	Koko kiinteä piste liukuluku Rationaalista Monimutkainen Pitkä intervalli
Teksti	Symbolinen merkkijono
Viite	Osoite Linkki Osoitin Kääre
Komposiitti	Algebrallinen tietotyyppi ( yleinen ) Luokka Tyyppituote ( Kirjoita Tuple rakenne ) Esine Konsolidointi ( tagged ) Järjestetty pari
abstrakti	joukko Lista Vuoro Pino Assosiatiivinen taulukko (näyttö, kartta ) Paljon multiset Tyyppi Kaavio
Muut	Looginen Alempi Korkeampi Polymorfinen Toimiva lueteltava Kokoelma Poikkeus Suku ( metaluokka ) Monad Semafori Virtaus mitätön
liittyvät aiheet	Abstrakti tietotyyppi primitiivinen tyyppi Tietorakenne Yleinen tyyppinen muuttuja Käyttöliittymä Rakentaja (OOP) Rakentaja (FP) Tyyppi rakentaja Tyyppivalu Prototyyppi Tyyppijärjestelmä