Tyyppiteoriassa tyyppikonstruktori on polymorfisesti tyypitetty muodollinen kielikonstrukti , joka rakentaa uusia tyyppejä vanhoista.
Esimerkkejä tyypillisistä tyyppimuodostajista ovat tuotetyypit , funktiotyypit ja luettelot . Alkuperäisiä tyyppejä edustavat nolla- ariteettityypin konstruktorit . Uusia tyyppejä voidaan rakentaa rekursiivisesti muodostavilla tyyppikonstruktoreilla.
Yksinkertaisesti kirjoitettua lambda-laskentaa voidaan pitää kielenä, jossa on yksityyppinen konstruktori, funktiotyyppinen konstruktori. Currying mahdollistaa kirjoitetussa lambda -laskennassa olevien tuotetyyppien käsittelemisen rivissä .
Pohjimmiltaan tyyppikonstruktori on n-ary - tyyppinen operaattori ( eng. type operator , operator over type), joka ottaa syötteeksi nollan tai useamman tyypin ja palauttaa toisen tyypin. Kun currya käytetään, -ary n -tyyppistä operaattoria voidaan esittää peräkkäisillä unaarityyppisten operaattorien sovelluksilla. Siksi tyyppioperaattoreita voidaan pitää yksinkertaisesti kirjoitettuna lambda-laskentana , jolla on yksi tyyppi, jota yleensä merkitään " *" (lue " tyyppi "), joka on kaikkien tyyppien tyyppi taustalla olevassa kielessä, jota tässä tapauksessa voidaan kutsua tyypillisiä tyyppejä erottaakseen ne tyyppityyppisistä operaattoreista omissa laskelmissaan - tyypit .
Tyyppioperaattoreiden käyttäminen perusteluna yksinkertaisesti kirjoitetulle lambda-laskimelle on kuitenkin enemmän kuin pelkkä formalisointi – se mahdollistaa korkeamman asteen tyyppioperaattorit (katso Suku (tyyppiteoria) #Esimerkit , polymorfismi korkeammissa suvuissa ). Tyyppioperaattorit kartoittavat lambda-kuution toiselle akselille , mikä johtaa yksinkertaisesti kirjoitettuun lambda-laskentaan, jossa on tyyppioperaattoreita, λ ω . Tyyppioperaattoreiden yhdistelmä polymorfisen lambda-lasken kanssa ( järjestelmä F ) muodostaa järjestelmän Fω .
Tyyppikonstruktoreita käytetään runsaasti tyyppitäydessä ohjelmoinnissa .
ML - perheen ohjelmointikielissä tyyppikonstruktoria edustaa funktio tyyppien yläpuolella - ts. funktio, joka ottaa tietyt tyypit syötteenä ja palauttaa toiset tyypit. Optimointikääntäjät suorittavat nämä toiminnot staattisesti, ts. käännösaikana (katso esimerkiksi MLton ).
ML :n klassiset murteet ( Standard ML , OCaml ) käyttävät monikkomerkintöjän -ary-tyyppisille konstruktoreille . Curried - tyyppiset konstruktorit ovat mahdollisia Haskellissa . ML :n klassiset murteet käyttävät postfix-syntaksia (esimerkiksi " ") luodessaan uusia tyyppejä , kun taas Haskell käyttää etuliitesyntaksia (" "). int listList Int
Nykyaikaisissa Standard ML :n toteutuksissa primitiiviset tyypit, kuten char, int, word, real, määritellään vakiokirjastomoduuleissa ( SML Basis ) nolla- tyyppisiksi konstruktoreiksi (katso lisätietoja ML:n numeroohjauksesta ). Sellaiset klassiset aggregaattityypit, kuten taulukot ja listat , toteutetaan samalla tavalla, mutta ne ovat jo unaarityyppisiä konstruktoreita vector(muuttumattomien elementtien taulukot), array(muuttuvien elementtien taulukot) ja list.
Standard ML : ssä on kaksi erilaista rakennetta tyyppikonstruktorien määrittämiseen -- typeja datatype. Ensimmäinen määrittelee aliaksen olemassa olevalle tyyppikonstruktorille tai niiden koostumukselle, toinen esittelee uuden algebrallisen tietotyypin omilla konstruktorillaan . Äskettäin määritellyt tyyppikonstruktorit voivat ottaa minkä tahansa määrän argumentteja. Tyyppimuuttujaa käytetään argumenttina tyyppikonstruktorille . Yhdellä tai useammalla argumentilla parametroituja tyyppejä kutsutaan polymorfisiksi ; tyypit ilman argumentteja ovat monomorfisia.
tietotyyppi t0 = T of int * real (* 0 argumenttia *) tyyppi ' a t1 = ' a * int (* 1 argumentti *) tietotyyppi ( ' a , ' b ) t2 = A | B :n ' a * ' b (* 2 argumenttia *) tyyppiä ( ' a , ' b , ' c ) t3 = ' a * ( ' b -> ' c ) (* 3 argumenttia *)Tässä on neljä tyyppistä konstruktoria: t0, t1, t2ja t3. Luodaksesi tyyppisiä 'a t1ja objekteja , 'a t2sinun on kutsuttava niiden rakentajat T ja A.B
Esimerkki tyyppikonstruktorien koostumuksesta, joka näyttää uusien tyyppien rakentamisen:
tyyppi t4 = t0 t1Tässä tyyppiä käytetään tyyppikonstruktorin tyyppimuuttujan todellisena arvona . Tuloksena oleva tyyppi on kahden elementin monikko , joista toinen on kokonaisluku, ja ensimmäinen muodostettiin soveltamalla konstruktoria kokonaisluvun ja reaaliluvun monikkoon. 'at1t0 T
Monimutkaisempi esimerkki:
kirjoita ' a t5 = ( ' a , ' a , ' a ) t3 t1Tyyppiobjektit t5ovat kahden elementin monikoita, joista ensimmäinen on tyypin erikoistapaus t3, jossa kaikkien kolmen argumentin on oltava identtisiä, ja toinen on kokonaisluku.
Haskellilla on jo kolme rakennetta tyyppikonstruktoreiden määrittämiseen - type, dataja newtype.
Rakenteita typeja käytetään datasamalla typetavalla Standard ML :ssä , mutta niissä on seuraavat erot: datatype
Esimerkki:
dataPoint a = Pt a a _Itse asiassa kaikilla ML -perheen kielillä tyyppi- ja arvokonstruktorit ovat eri nimiavaruuksissa, joten samaa tunnistetta voidaan käyttää tällaisissa tapauksissa:
data Piste a = Piste a aAlgebrallisen tyypin käytöllä on jonkin verran suorituskykyä, koska arvon rakentajaa käytetään dynaamisesti. Sen korvaaminen tyyppialiaksella (määritetty kautta type) parantaa tehokkuutta, mutta heikentää tyyppiturvallisuutta (koska on mahdotonta hallita superstrukturoidun tyypin ainutlaatuisia ominaisuuksia, jotka rajoittavat sen käyttöä suhteessa taustalla olevaan tyyppiin). Tämän ongelman ratkaisemiseksi Haskell lisäsi rakenteen newtype:
uusityyppi Piste a = Piste ( a , a )Tällä tavalla määritellyllä tyypillä voi olla yksi ja vain yksi arvokonstruktori , jolla on täsmälleen yksi parametri. Lähdekoodissa tällaisia tyyppejä käytetään identtisesti kautta määritettyjen tyyppien kanssa data, mikä antaa tyypin turvallisuuden. Sitä ei kuitenkaan ole erillisenä kokonaisuutena suoritettavassa koodissa newtype, vaan sen konstruktoriparametrin tyyppiä käytetään. Tässä tapauksessa toimintojen suoritettava koodi on Point ayhtä tehokas kuin monikkooperaatioiden koodi (a, a).
| Tietotyypit | |
|---|---|
| Käsittämätön | |
| Numeerinen | |
| Teksti | |
| Viite | |
| Komposiitti | |
| abstrakti | |
| Muut | |
| liittyvät aiheet | |