Tyyppijärjestelmä on ohjelmointikielten sääntöjoukko , joka määrittää ominaisuuksia, joita kutsutaan tyypeiksi , erilaisille ohjelman muodostaville rakenteille , kuten muuttujille , lausekkeille , funktioille tai moduuleille . Tyyppijärjestelmän päätehtävänä on vähentää ohjelmien virheiden määrää [1] määrittelemällä rajapinnat ohjelman eri osien välille ja tarkistamalla sitten näiden osien vuorovaikutuksen johdonmukaisuus. Tämä tarkistus voi tapahtua staattisesti ( käännösaikana ) tai dynaamisesti ( ajon aikana ).) ja olla myös molempien yhdistelmä.
Pierce mukaan tyyppijärjestelmä on päätettävissä oleva syntaktinen menetelmä , jolla todistetaan tiettyjen ohjelmien käyttäytymisen puuttuminen luokittelemalla konstruktit laskettujen arvojen tyyppien mukaan [2] .
Esimerkki yksinkertaisesta tyyppijärjestelmästä on nähtävissä C -kielessä . C - ohjelman osat kirjoitetaan funktiomäärityksinä . Toiminnot kutsuvat toisiaan. Toiminnon käyttöliittymä määrittää funktion nimen ja luettelon arvoista, jotka välitetään sen runkoon. Kutsuva funktio olettaa sen funktion nimen, jota se haluaa kutsua, ja muuttujien nimet, jotka sisältävät arvot, jotka se haluaa välittää. Ohjelman suorituksen aikana arvot sijoitetaan väliaikaiseen tallennustilaan ja sitten suoritus välitetään kutsutun funktion runkoon. Kutsuttu toimintokoodi hakee arvoja ja käyttää niitä. Jos käskyt funktion rungossa on kirjoitettu olettaen, että niille pitäisi välittää kokonaislukuarvo käsittelyä varten, mutta kutsuva koodi välitti liukulukuluvun, niin kutsuttu funktio arvioi väärän tuloksen. C-kääntäjä tarkistaa kullekin välitetylle muuttujalle määritellyt tyypit verraten kullekin muuttujalle määritettyjä tyyppejä kutsutun funktion rajapinnassa. Jos tyypit eivät täsmää, kääntäjä luo käännösaikavirheen.
Teknisesti tyyppijärjestelmä määrittää tyypin jokaiselle laskennalliselle arvolle ja sitten seuraamalla näiden laskelmien järjestystä yrittää tarkistaa tai todistaa, ettei tyyppisovitusvirheitä ole . Tietyn tyyppinen järjestelmä voi määrittää, mikä aiheuttaa virheen, mutta yleensä tavoitteena on estää operaatioita, jotka olettavat tiettyjä parametrien ominaisuuksia, vastaanottamasta parametreja, joille nämä toiminnot eivät ole järkeviä – loogisten virheiden estäminen . Lisäksi se estää myös muistiosoitevirheet .
Tyyppijärjestelmät määritellään yleensä osaksi ohjelmointikieliä ja ne on rakennettu niiden tulkkeihin ja kääntäjiin. Kielen tyyppijärjestelmää voidaan kuitenkin laajentaa erikoistyökaluilla , jotka suorittavat lisätarkistuksia kielen alkuperäisen kirjoitussyntaksin perusteella.
Kääntäjä voi myös käyttää staattista arvotyyppiä optimoidakseen tallennusta ja valitakseen toimintojen algoritmisen toteutuksen tälle arvolle. Esimerkiksi monissa C-kääntäjissä tyyppiä edustaa float 32 bittiä IEEE:n yhden tarkkuuden liukulukuoperaatioiden määrityksen mukaan . Tämän perusteella tämän tyyppisille arvoille (yhteen-, kertolasku- ja muut toiminnot) käytetään erityistä mikroprosessoriohjeiden sarjaa .
Tyypeille asetettujen rajoitusten määrä ja niiden laskentatapa määräävät kielen kirjoituksen. Lisäksi tyyppipolymorfismin tapauksessa kieli voi myös määrittää kullekin tyypille erilaisten algoritmien toiminnan. Tyyppijärjestelmien tutkimus on tyyppiteoriaa , vaikka käytännössä ohjelmointikielen tietty tyyppijärjestelmä perustuu tietokonearkkitehtuurin ominaisuuksiin, kääntäjän toteutukseen ja kielen yleiskuvaan.
Tyyppijärjestelmien muodollinen perustelu on tyyppiteoria . Ohjelmointikieli sisältää tyyppijärjestelmän tyyppitarkistuksen suorittamiseksi käännösaikana tai ajon aikana , joka vaatii eksplisiittisiä tyyppimäärittelyjä tai päättelee niistä itsestään. Mark Manasse muotoili ongelman seuraavasti [3] :
Suurin ongelma, jonka tyyppiteoria ratkaisee, on varmistaa ohjelmien järkeä. Tyyppiteorian suurin ongelma on, että mielekkäät ohjelmat eivät välttämättä toimi niin kuin on tarkoitettu. Tämän jännityksen seurauksena on tehokkaampien tyyppisten järjestelmien etsiminen.
Alkuperäinen teksti (englanniksi)[ näytäpiilottaa] Tyyppiteorian käsittelemä perusongelma on varmistaa, että ohjelmilla on merkitys. Tyyppiteorian perustana on se, että merkityksellisille ohjelmille ei välttämättä ole liitetty ongelmamerkityksiä. Rikkaamman tyyppisten järjestelmien etsintä johtuu tästä jännityksestä. — Mark Massey [3]Tyypin määritystoiminto, jota kutsutaan typingiksi, antaa merkityksen bittijonoille , kuten arvolle tietokoneen muistissa , tai objekteille , kuten muuttujalle . Tietokone ei pysty erottamaan esimerkiksi muistissa olevaa osoitetta koodikäskystä tai merkkiä kokonaisluvusta tai liukulukusta , koska näitä eri merkityksiä edustavilla bittijonoilla ei ole mitään ilmeisiä ominaisuuksia, joiden avulla voidaan tehdä oletuksia niiden merkityksestä. Tyyppibittien määrittäminen merkkijonoihin tarjoaa tämän ymmärrettävyyden, jolloin ohjelmoitava laitteisto muuttuu merkkijärjestelmäksi, joka koostuu kyseisestä laitteistosta ja ohjelmistosta.
Tyypintarkistus- ja rajoitusprosessi - tyypin tarkistus tai tyypin tarkistus - voidaan tehdä joko käännösaikana staattinen kirjoitus) tai ajon aikana (dynaaminen kirjoitus). Myös väliratkaisut ovat mahdollisia (vrt. sarjakirjoitus ).
Jos kielimäärittely edellyttää, että kirjoitussäännöt on tiukasti toteutettu (eli sallitaan tavalla tai toisella vain sellaiset automaattiset tyyppimuunnokset, jotka eivät menetä tietoja), tällaista kieltä kutsutaan vahvasti kirjoitetuksi ; ), muuten heikosti kirjoitetuksi . Nämä termit ovat ehdollisia, eikä niitä käytetä muodollisissa perusteluissa.
Kieltä kutsutaan kirjoitetuksi, jos kunkin toiminnon määrittelyssä määritellään tietotyypit, joihin tätä toimintoa voidaan soveltaa, mikä tarkoittaa, että sitä ei voida soveltaa muihin tyyppeihin [4] . Esimerkiksi tiedot, joita " tämä lainattu teksti " edustaa , ovat tyyppiä " строка". Useimmissa ohjelmointikielissä luvun jakaminen merkkijonolla ei ole järkevää, ja useimmat nykyaikaiset kielet hylkäävät ohjelman, joka yrittää suorittaa tällaisen toiminnon. Joillakin kielillä merkityksetön toiminto havaitaan kääntämisen aikana ( staattinen kirjoitus ) ja kääntäjä hylkää sen. Toisissa se havaitaan suorituksen aikana ( dynaaminen kirjoittaminen ), mikä tekee poikkeuksen .
Tyypitettyjen kielten erikoistapaus ovat yksityyppiset kielet ( eng. single-type language ), eli kielet, joilla on yksi tyyppi. Nämä ovat yleensä komentosarja- tai merkintäkieliä , kuten REXX ja SGML , joiden ainoa tietotyyppi on merkkijono, jota käytetään edustamaan sekä merkki- että numeerista tietoa.
Tyypittämättömät kielet, toisin kuin kirjoitetut, antavat sinun suorittaa minkä tahansa toiminnon mille tahansa datalle, joka niissä esitetään mielivaltaisen pituisilla bittiketjuilla [4] . Useimmat kokoonpanokielet ovat kirjoittamattomia . Esimerkkejä korkean tason kirjoittamattomista kielistä ovat BCPL , BLISS , Forth , Refal .
Käytännössä harvoja kieliä voidaan pitää tyyppiteorian kannalta kirjoitettuina (sallivat tai hylkäävät kaikki toiminnot), useimmat nykyaikaiset kielet tarjoavat vain jonkinasteista tyyppiä [4] . Monet teolliset kielet tarjoavat mahdollisuuden ohittaa tai katkaista tyyppijärjestelmän, mikä vaihtaa tyyppiturvallisuutta ohjelman suorittamisen tarkempaan hallintaan ( kirjoitussana ).
Termi "polymorfismi" viittaa koodin kykyyn toimia useiden erityyppisten arvojen kanssa tai saman tietorakenteen eri esiintymien kykyä sisältää erityyppisiä elementtejä. Jotkin tyyppijärjestelmät mahdollistavat polymorfismin mahdollisesti parantavan koodin uudelleenkäyttöä : monimuotoisissa kielissä ohjelmoijien tarvitsee toteuttaa tietorakenteita, kuten luettelo tai assosiatiivinen taulukko vain kerran, eikä heidän tarvitse kehittää yhtä toteutusta jokaiselle suunnittelemansa elementtityypille. varastoida rakenteita. Tästä syystä jotkut tietojenkäsittelytieteilijät kutsuvat joskus tiettyjen polymorfismin muotojen käyttöä " yleiseksi ohjelmoimiseksi ". Polymorfismin perustelut tyyppiteorian näkökulmasta ovat käytännössä samat kuin abstraktion , modulaarisuuden ja joissain tapauksissa datan alatyypityksen .
Useita erikoistyyppisiä järjestelmiä on kehitetty käytettäväksi tietyissä olosuhteissa tietyn tiedon kanssa sekä ohjelmien staattiseen analysointiin . Ne perustuvat pääosin muodollisen tyyppiteorian ideoihin ja niitä käytetään vain osana tutkimusjärjestelmiä.
Eksistentiaaliset tyypit eli eksistentiaalisen kvantisoijan (olemassaolokvantioijan) määrittelemät tyypit ovat tyyppitason kapselointimekanismi : se on yhdistelmätyyppi , joka piilottaa jonkin tyypin toteutuksen koostumuksessaan.
Eksistentiaalisen tyypin käsitettä käytetään usein yhdessä tietuetyypin käsitteen kanssa edustamaan moduuleja ja abstrakteja tietotyyppejä , koska niiden tarkoitus on erottaa toteutus rajapinnasta. Esimerkiksi tyyppi T = ∃X { a: X; f: (X → int); }kuvaa moduulirajapinta (samalla allekirjoituksella varustettujen moduulien perheitä), jolla on tyypin data-arvo Xja funktio, joka ottaa täsmälleen samantyyppisen parametrin Xja palauttaa kokonaisluvun. Toteutus voi olla erilainen:
Molemmat tyypit ovat yleisemmän eksistentiaalityypin alatyyppejä Tja vastaavat konkreettisesti toteutettuja tyyppejä, joten mikä tahansa arvo, joka kuuluu jompaankumpaan niistä, kuuluu myös tyyppiin T. Jos t on tyypin arvo T, se t.f(t.a)läpäisee tyyppitarkistuksen riippumatta siitä, mihin abstraktiin tyyppiin se kuuluu X. Tämä antaa joustavuutta tiettyyn toteutukseen sopivien tyyppien valinnassa, koska ulkoiset käyttäjät pääsevät vain käyttöliittymätyypin (eksistentiaaliseen) arvoihin ja ovat erillään näistä muunnelmista.
Yleensä tyyppiyhdenmukaisuuden tarkistus ei voi määrittää, mihin eksistentiaaliseen tyyppiin tietty moduuli kuuluu. Yllä olevassa esimerkissä intT { a: int; f: (int → int); }sillä voi olla myös tyyppi ∃X { a: X; f: (int → int); }. Yksinkertaisin ratkaisu on määrittää jokaiselle moduulille eksplisiittisesti sen oletettu tyyppi, esimerkiksi:
Vaikka abstrakteja tietotyyppejä ja moduuleja on käytetty ohjelmointikielissä pitkään, muodollinen malli eksistentiaalisista tyypeistä rakennettiin vasta vuonna 1988 [5] . Teoria on toisen asteen tyyppinen lambda -laskenta, joka on samanlainen kuin systeemi F , mutta eksistentiaalinen kvantifiointi universaalin kvantifioinnin sijaan .
Eksistentiaaliset tyypit ovat eksplisiittisesti saatavilla Haskell - kielen kokeellisena laajennuksena , jossa ne ovat erityinen syntaksi , jonka avulla voit käyttää tyyppimuuttujaa algebrallisessa tyyppimäärittelyssä siirtämättä sitä tyyppikonstruktorin allekirjoitukseen , eli lisäämättä sen ariteettia [ 6] . Java - kieli tarjoaa rajoitetun muodon eksistentiaalisille tyypeille yleismerkin kautta . Klassista ML - tyylistä let-polymorfismia toteuttavissa kielissä eksistentiaalisia tyyppejä voidaan simuloida niin sanottujen " tyyppiindeksoitujen arvojen " [7] avulla .
Monet staattiset tyyppijärjestelmät, kuten C- ja Java-järjestelmät, vaativat tyyppimäärityksen : ohjelmoijan on nimenomaisesti määritettävä kullekin muuttujalle tietty tyyppi. Toiset, kuten ML :ssä ja Haskellissa käytetty Hindley-Milner- tyyppijärjestelmä , tekevät tyyppipäätelmän : kääntäjä päättelee muuttujien tyypit sen perusteella, kuinka ohjelmoija käyttää näitä muuttujia.
Esimerkiksi funktiolle f(x,y), joka suorittaa yhteenlasku- xja y, kääntäjä saattaa päätellä, että xja ytäytyy olla numeroita - koska yhteenlaskutoiminto on määritetty vain numeroille. Siksi funktion kutsuminen jossain ohjelmassa fmuille kuin numeerisille parametreille (esimerkiksi merkkijonolle tai listalle) merkitsee virhettä.
Numeeriset ja merkkijonovakiot ja lausekkeet ilmaisevat yleensä tyyppiä tietyssä kontekstissa. Lauseke 3.14voi esimerkiksi tarkoittaa reaalilukua , kun taas se [1,2,3]voi olla kokonaislukuluettelo – yleensä taulukko .
Yleisesti ottaen tyyppipäätelmä on mahdollista, jos se on pohjimmiltaan päätettävissä tyyppiteoriassa. Lisäksi, vaikka päättäminen on ratkaisematon tietyn tyyppiselle teorialle, päättäminen on usein mahdollista monille todellisille ohjelmille. Haskell - tyyppinen järjestelmä , joka on muunnelma Hindley-Milner- tyyppisestä järjestelmästä , on Fω-järjestelmän rajoitus niin sanottuihin ensimmäisen asteen polymorfisiin tyyppeihin, joista voidaan päätellä. Monet Haskell-kääntäjät tarjoavat mielivaltaisen järjestyksen polymorfismin laajennuksena, mutta tämä tekee tyyppipäätelmästä mahdotonta, joten tarvitaan eksplisiittinen tyyppimääritys. Tyyppiyhdenmukaisuuden tarkistus on kuitenkin päätettävissä, ja ohjelmille, joilla on ensisijainen polymorfismi, tyypit ovat edelleen johdettavissa.
Joillakin kielillä, kuten C# , on yhtenäinen tyyppijärjestelmä [8] . Tämä tarkoittaa, että kaikki kielen tyypit primitiivisiin asti peritään yhdestä juuriobjektista (C#:n tapauksessa luokasta Object). Javalla on useita primitiivityyppejä, jotka eivät ole objekteja. Näiden lisäksi Java tarjoaa myös kääreobjektityyppejä, jotta kehittäjä voi käyttää primitiivi- tai objektityyppejä parhaaksi katsomallaan tavalla.
Tyyppiyhdenmukaisuuden tarkistusmekanismi staattisesti kirjoitetussa kielessä tarkistaa, että mikä tahansa lauseke vastaa tyyppiä, jota se esiintyy kontekstissa. Esimerkiksi tyypin määrityskäskyssä lausekkeelle päätellyn tyypin on vastattava muuttujalle ilmoitettua tai pääteltyä tyyppiä . Yhteensopivuusmerkintä, jota kutsutaan yhteensopivuudeksi , on kunkin kielen oma. x := eex
Jos eja xovat samaa tyyppiä ja osoitus on sallittu tälle tyypille, lauseke on laillinen. Siksi yksinkertaisimmissa tyyppijärjestelmissä kysymys kahden tyypin yhteensopivuudesta yksinkertaistuu kysymykseksi niiden tasa -arvosta ( ekvivalenssi ). Eri kielillä on kuitenkin erilaiset kriteerit kahden lausekkeen tyyppiyhteensopivuuden määrittämiseksi. Nämä ekvivalenssiteoriat vaihtelevat kahden ääripään välillä: rakenteelliset järjestelmät , joissa kaksi tyyppiä ovat ekvivalentteja, jos ne kuvaavat samaa arvon sisäistä rakennetta; ja nominatiivityyppiset järjestelmät , joissa syntaktisesti erilaiset tyypit eivät ole koskaan ekvivalentteja ( eli kaksi tyyppiä ovat samanarvoisia vain, jos niiden tunnisteet ovat samat) .
-alatyypeillä varustetuilla kielillä yhteensopivuussäännöt ovat monimutkaisempia. Jos esimerkiksi on tyypin alatyyppi , tyypin arvoa voidaan käyttää kontekstissa, joka odottaa tyypin arvon , vaikka käänteinen ei olisi totta. Kuten vastaavuudenkin kohdalla, alatyyppisuhteet vaihtelevat eri kielissä, ja monet sääntöjen muunnelmat ovat mahdollisia. Parametrisen tai tilanneperäisen polymorfismin esiintyminen kielessä voi myös vaikuttaa tyyppien yhteensopivuuteen. ABAB
Jotkut ohjelmoijat suosivat staattisia järjestelmiä, toiset dynaamisia . Staattisesti kirjoitettujen kielten signaalityyppien johdonmukaisuusvirheet käännöshetkellä voivat tuottaa tehokkaammin suoritettavaa koodia, ja tällaisille kielille osuvampi viimeistely IDE:issä on mahdollista . Dynaamisen kirjoittamisen kannattajat väittävät, että ne soveltuvat paremmin nopeaan prototyyppiin ja että tyyppisovitusvirheet ovat vain pieni osa ohjelmien mahdollisista virheistä [9] [10] . Toisaalta staattisesti kirjoitetuissa kielissä eksplisiittistä tyyppimääritystä ei yleensä vaadita, jos kieli tukee tyyppipäätelmää , ja jotkin dynaamisesti kirjoitetut kielet suorittavat ajonaikaisia optimointeja [11] [12] , usein käyttämällä osittaista tyyppiä. johtopäätös [13] .
| Tietotyypit | |
|---|---|
| Käsittämätön | |
| Numeerinen | |
| Teksti | |
| Viite | |
| Komposiitti | |
| abstrakti | |
| muu | |
| liittyvät aiheet | |