Tyyppinen muuttuja

Tyyppimuuttuja ( tyyppimuuttuja ) ohjelmointikielissä ja tyyppiteoriassa  on muuttuja , joka voi ottaa arvon tietotyypeistä .

Tyyppimuuttujaa käytetään algebrallisen tietotyypin määrittelyssä samalla tavalla kuin parametria funktiomäärittelyssä , mutta sitä käytetään tietotyypin välittämiseen välittämättä itse dataa. Kreikkalaisia ​​merkkejä käytetään perinteisesti tyyppimuuttujien tunnisteina tyyppiteoriassa (vaikka monet ohjelmointikielet käyttävät latinalaisia ​​aakkosia ja sallivat pidemmät nimet).

Esimerkki

Seuraavassa standardin ML :n polymorfisen tyypin " list " määritelmässä tunniste (lausutaan "alpha") on tyyppiä [2] oleva muuttuja : 'a

tietotyyppi 'a list = nolla | :: ' a * ' luettelosta

Tätä polymorfista tyyppiä käytettäessä tyyppimuuttujaksi korvataan tietty tyyppi, joten ohjelmassa voidaan muodostaa monia monomorfisia tyyppejä: string list, int list, int list listja niin edelleen. Tällä korvauksella jokainen viittaus tyyppimuuttujaan korvataan samalla tyypillä. Saatua tyyppitietoa käytetään ohjelman tarkistamiseen ja optimointiin , minkä jälkeen se yleensä poistetaan, jotta sama kohdekoodi käsittelee alun perin erityyppisiä objekteja (mutta tästä säännöstä on poikkeuksia, erityisesti MLtonissa ).

Jos polymorfinen tyyppi parametroidaan useilla tyyppimuuttujilla, niihin substituoidut tyypit voivat olla joko erilaisia ​​tai identtisiä, mutta korvaussääntöä noudatetaan. Jos tämä tyyppi on esimerkiksi:

tietotyyppi ( 'a , 'b ) t = Yksi 'a | : sta Double of 'a * 'a | Pari ' a * ' b

muotoile näin:

kirjoita t_ir = ( int , real ) t

sitten Single(4), Double(4,5)ja Pair(4,5.0)ovat kelvollisia tyypin arvoja t_ir, ja arvon Single(5.0)muodostaminen johtaa kirjoitusvirheeseen, koska parametrin 'aarvo on " int".

Linkittäminen ja kvantifiointi

Minkä tahansa tyyppimuuttujan laajuus on sidottu tiettyyn kontekstiin [3] [4] . Seuraavassa esimerkissä tunnistetta 'akäytetään itsenäisesti kahdessa allekirjoituksessa, mikä tarkoittaa, että se ei vaadi todellisten rivityyppien yhtäläisyyttä määritelmien välillä:

val foo : 'a -> 'a val bar : 'a -> 'a

Tämä käy selväksi, kun käytetään eksplisiittisen sidostyypin ( eksplisiittisen laajuuden tai eksplisiittisen rajauksen ) tyyppistä muuttujaa:

val foo : [ 'a ] 'a -> 'a val bar : [ 'a ] 'a -> 'a

Sidonta rajoittaa tietyn tyyppisen muuttujan laajuutta.

Klassisissa ML-murteissa tyyppimuuttujien eksplisiittinen sitominen on valinnainen ominaisuus, eikä useimpia toteutuksia tueta tarpeettomana - niissä sitominen on implisiittistä tyyppivähennyksessä , mikä tulee mahdolliseksi Hindley-Milner-järjestelmän varhaisten versioiden rajoitusten vuoksi . Koko järjestelmässä F tämä ilmoitus kirjoitetaan muodossa . Tällaista merkintää kutsutaan prenex-normaalimuodoksi . Iso kirjain tässä merkinnässä tarkoittaa tyyppikerroksen funktiota ( type-level function ), jonka parametri on tyyppimuuttuja. Kun tämä muuttuja on korvannut tietyn tyypin, tämä funktio palauttaa monomorfisen arvotason funktion ( arvotason funktio ). Prenex on tyyppimuuttujan eksplisiittinen sidos, joka on etuliitteenä tyyppiallekirjoitukseen. Hindley-Milner-järjestelmän varhaiset versiot sallivat vain prenex-muodon, toisin sanoen ne vaativat, että tyyppimuuttuja oli instantioitu tietyllä arvolla ennen kuin funktiokutsua tarvittiin. Tätä rajoitusta kutsutaan prenex-polymorfismiksi  - se ei ainoastaan ​​yksinkertaista suuresti tyyppisovitusmekanismia , vaan myös mahdollistaa kaikkien tai melkein kaikkien (murteesta riippuen) ohjelman tyyppien päättelemisen .

Tyyppimuuttujien yksinkertaisinta sidontaa kutsutaan niiden kvantifiointiksi . Kaksi tapausta erottuu:

  • tyyppimuuttujan toiminta ulottuu koko tyyppimäärittelyyn: ['a, 'b] 'a -> 'b -> 'amatemaattisesti tällainen tyyppi kirjoitetaan universaalin kvantisoijan kautta - - siksi tällaista tyyppimuuttujaa kutsutaan "universaalisesti kvantitoiduksi" ja koko tyyppiä kutsutaan "universaalisesti polymorfiseksi";
  • tyyppimuuttujan vaikutus ulottuu vain osaan tyyppimäärittelystä: ['a] 'a -> (['b] 'b -> 'a)matemaattisesti tällainen tyyppi kirjoitetaan eksistentiaalisen kvantisoijan kautta - - siksi tällaista muuttujaa kutsutaan "eksistenttiaalisesti kvantitoiduksi" ja koko tyyppiä kutsutaan "eksistentiaaliseksi".

Ei kaikissa tapauksissa universaalisti polymorfisen tyypin "muuttaminen" eksistentiaaliksi tyypiksi anna käytännöllistä tyyppiä tai havaittavia eroja universaalista polymorfismista, mutta joissain tapauksissa eksistentiaalityyppien käyttö nostaa parametrisen polymorfismin ensiluokkaiselle tasolle , ts. mahdollistaa polymorfisten funktioiden välittämisen ilman sitoutumista parametreiksi muihin funktioihin (katso ensimmäisen luokan polymorfismi ). Klassinen esimerkki on heterogeenisen listan toteutus (katso wikikirja). Tyyppien nimenomainen huomautus tulee tässä tapauksessa pakolliseksi, koska tyyppipäätelmä luokan 2 polymorfismille on algoritmisesti ratkaisematon [5] .

Käytännössä universaalisti polymorfiset tyypit antavat tietotyypin yleistyksen ja eksistentiaaliset tyypit - tietotyypin abstraktion [6] .

Haskell erottaa useita tiloja (saatavilla kielilaajennuksina): Rank2Types- moodi sallii vain jotkin eksistentiaalityyppiset muodot, jotka avaavat polymorfismin korkeintaan 2. luokkaa korkeammalla, jolle tyyppipäätelmä on vielä päätettävissä; RankNTypes- moodi mahdollistaa universaalin kvantisoijan ( forall a) siirtämisen funktionaalisten tyyppien sisällä , jotka ovat osa monimutkaisempia allekirjoituksia [7] , ImpredicativeTypes -moodi mahdollistaa mielivaltaiset eksistentiaaliset tyypit [8] .

OCaml toteuttaa eksistentiaalisen kvantifioinnin tuen ratkaisulla, jota kutsutaan "paikallisesti abstrakteiksi tyypeiksi" [ 9 ] .

Standard ML -spesifikaatio määrittelee erityisen kvantifioinnin joillekin sisäänrakennetuille toiminnoille. Sen syntaksia ei säännellä ja se eroaa kielitoteutuksista (useimmiten se on yksinkertaisesti piilotettu). Esimerkiksi sisäänrakennetun lisäystoiminnon allekirjoitus voidaan yksinkertaistaa seuraavasti:

val + : [ int , sana , real ] 'a * 'a -> 'a

Tämä semantiikka toteuttaa ad-hoc-polymorfismin primitiivisen muodon  - yhdistäen useita fyysisesti erilaisia ​​lisäysoperaatioita yhden tunnisteen " +" alle. OCamlin kehittäjät hylkäsivät tämän ratkaisun poistamalla kokonaan ad-hoc-polymorfismin kielestä ( yleistetyt algebralliset tietotyypit ilmestyivät myöhemmissä versioissa ).

1980-luvun lopulla ilmestyi Hindley-Milner- laajennus , joka tarjosi mahdollisuuden rajoittaa tarvittaessa minkä tahansa tyyppimuuttujan arvoaluetta äskettäin määritellyissä tyyppi- tyyppiluokissa . Tyyppiluokka rajoittaa sallittuja kirjoituskonteksteja tiukemmin sallien tyyppimuuttujan ilmentymisen vain tyypeillä, jotka kuuluvat nimenomaisesti määritettyyn luokkaan.

Tämä laajennus otettiin ensimmäisen kerran käyttöön Haskell-kielen ytimessä , esimerkiksi tasa-arvovertailuoperaattorissa on seuraava allekirjoitus :

( == ) :: ( Eq a ) => a -> a -> Bool

Seuraavan sukupolven kielen - seuraajan ML [1] - projekti kieltäytyy tyyppipäätelmän  tarpeesta , luottaen eksplisiittiseen (manifest-) tyyppimerkintään (mukaan lukien tyyppimuuttujien eksplisiittinen sitominen), joka tarjoaa suoran tuen koko järjestelmälle F, jossa on ensimmäinen luokan polymorfismi ja joukko laajennuksia, mukaan lukien alatyyppien ja eksistentiaalityyppien hierarkiat [1] .

Erikoistyyppimuuttujat

Pääasiallinen tyyppimuuttujien luokka, jota käytetään kaikilla ML -perheen kielillä, ovat sovellustyyppiset muuttujat, jotka voivat ottaa arvoja kaikista tietyssä kielessä sallituista tyypeistä. Klassisissa murteissa niitä merkitään syntaktisesti " 'a" (aakkosnumeerinen tunniste, joka alkaa aina yhdellä heittomerkillä ); Haskellissa muodossa " a" (aakkosnumeerinen tunniste, joka alkaa aina pienellä kirjaimella).

Lisäksi läpi ML :n historian on erotettu erityisiä tyyppimuuttujien alaluokkia.

Muuttujat, joiden tasa-arvo voidaan tarkistaa (tai vastaavan tyyppiset muuttujat, yhtäläisyystyypin muuttujat ) - voivat ottaa arvoja kaikkien tyyppien joukosta, joiden tasa-arvo voidaan tarkistaa ( englanniksi  tasa-arvotyypit ). Niiden käyttö mahdollistaa tasa-arvovertailuoperaation soveltamisen polymorfisten tyyppien esineisiin. Ne on merkitty " ''a" (aakkosnumeerinen tunniste, joka alkaa aina kahdella heittomerkillä ). Mielenkiintoista on, että yksi alkuperäisistä tavoitteista, joita varten tyyppiluokkia kehitettiin, oli juuri tällaisten tyyppimuuttujien yleistäminen Standard ML :stä [10] . Niitä on kritisoitu toistuvasti kielen määrittelyn ja kääntäjien käyttöönoton merkittävästä (ja väitetysti perustellusta) monimutkaisuudesta (puolet määritelmän sivuista sisältää niihin yhden tai toisen muutoksen) [11] . Periaatteessa monimutkaisten abstraktien tietotyyppien tasa-arvon tarkistaminen ei ole suositeltavaa, koska tällaiset tarkistukset voivat viedä huomattavan paljon aikaa. Siksi ML -perheen myöhemmistä kielistä tuki tasa-arvotestauksen mahdollistaville muuttujille poistettiin. Haskell käyttää sen sijaan tyyppiluokkaa Eq a .

Pakolliset tyyppimuuttujat tarjosivat ad hoc - ratkaisun sivuvaikutuksiin liittyvään tyyppiturvaongelmaan kielessä , jossa on parametrinen polymorfismi . Tätä ongelmaa ei esiinny puhtailla kielillä ( Haskell , Clean ), mutta epäpuhtailla kielillä ( standardi ML , OCaml ) viitepolymorfismi uhkaa kirjoitusvirheitä [3] [4] . Pakolliset tyyppimuuttujat olivat osa SML'90-määritelmää, mutta niillä ei ollut omaa merkitystään sen jälkeen, kun " arvorajoitus " keksittiin , josta tuli osa tarkistettua SML'97-määritelmää. SML'97:n pakottavien tyyppimuuttujien syntaktinen tuki säilytettiin taaksepäin yhteensopivuuden vuoksi aiemmin kirjoitetun koodin kanssa, mutta nykyaikaiset toteutukset käsittelevät niitä samalla tavalla kuin aplikatiivisia. Merkitään " " (aakkosnumeerinen tunniste, joka alkaa aina heittomerkillä ja alaviivalla) [3] . '_a

Heikkotyyppisiä muuttujia käytettiin SML/NJ-kääntäjässä vaihtoehtona pakollisille tyyppimuuttujille, mikä tarjosi paljon enemmän tehoa (tarkemmin sanottuna vähemmän rajoituksia). Merkitään " '1a", " '2a" ja niin edelleen (aakkosnumeerinen tunniste, joka alkaa aina heittomerkillä ja numerolla). Välittömästi heittomerkkiä seuraava numero osoitti tyyppimuuttujan "heikkouden" asteen. Kuten pakottavia tyyppimuuttujia, niitä käsitellään nyt samalla tavalla kuin aplikatiivisia muuttujia. [3]

Muistiinpanot

  1. ↑ 1 2 3 ML2000, 1999 .
  2. ↑ Tässä eksplisiittiselle sidokselle ( eksplisiittiselle sidokselle ) käytetään tyyppimuuttujan nykyistä syntaksia, joka on hyväksytty seuraajassa ML -projektissa [1] : ['a]. Koska Haskell nimesi tämän syntaksin syntaktiseksi sokerin yli tyypin , avainsanaList otettiin käyttöön ilmoittamaan tyyppimuuttujat . forall
  3. ↑ 1 2 3 4 MacQueen - TypeChecking .
  4. ↑ 12 MLton - Scoping .
  5. ↑ haskell_existentials .
  6. ↑ Cardelli, Wegner, 1985 .
  7. ↑ haskell_rankNtypes .
  8. ↑ haskell_impredicative_types .
  9. ↑ OCaml-laajennukset. 7.13 Paikallisesti abstraktit tyypit
  10. ↑ Philip Wadler, Stephen Blott. Kuinka tehdä ad hoc -polymorfismista vähemmän ad hoc . – 1988.
  11. ↑ Andrew W. Appel. Standard ML:n kritiikki . — Princetonin yliopisto, tarkistettu versio CS-TR-364-92:sta, 1992.

Kirjallisuus

Linkit

 Tietotyypit
Käsittämätön
Numeerinen
Teksti
Viite
Komposiitti
abstrakti
Muut
liittyvät aiheet