Riippuvainen tyyppi

Riippuvainen tyyppi ( englanniksi riippuvainen tyyppi ) tietojenkäsittelytieteessä ja logiikassa on tyyppi , joka riippuu jostain arvosta. Riippuvilla tyypeillä on keskeinen rooli intuitionistisessa tyyppiteoriassa ja toiminnallisten ohjelmointikielten , kuten ATS , Agda , Epigram ja Idris , rakentamisessa .

Esimerkiksi tyyppi, joka kuvaa n - lukua reaalilukuja, on riippuvainen, koska se "riippuu" n:n arvosta .

Sen päättäminen, ovatko riippuvaiset tyypit samanarvoisia ohjelmassa, voi vaatia laskennan. Jos mielivaltaiset arvot sallitaan riippuvaisissa tyypeissä, tyyppitasa-arvopäätös voi sisältää kahden mielivaltaisen ohjelman työn tuloksen tasa-arvon tarkistamisen. Siten tyypin tarkistuksesta tulee ratkaisematon tehtävä .

Curry-Howard-isomorfismin avulla voit rakentaa tyyppejä ilmaisemaan mielivaltaisen monimutkaisia matemaattisia ominaisuuksia. Jos toimitetaan rakentava todistus siitä , että tyyppi on "asuttu" (eli kyseisellä tyypillä on vähintään yksi arvo), kääntäjä pystyy tarkistamaan tämän todisteen ja muuttamaan sen suoritettavaksi koodiksi, joka arvioi arvon. Todistustarkistuksen olemassaolo tekee riippuvaisesti kirjoitetuista kielistä samanlaisia kuin todistusautomaatioohjelmisto (kuten interaktiivinen Coq -lauseen todistaja ).

Lambda-kuutiojärjestelmät

Henk Barendregt kehitti lambda-kuution keinona luokitella tyyppijärjestelmät kolmella akselilla. Jokainen kuutiokaavion kahdeksasta kulmasta vastaa tyyppijärjestelmää. Kuution köyhimmässä kärjessä on yksinkertaisesti kirjoitettu lambda -laskenta ja rikkaimmassa kärjessä on rakennuslaskenta . Kuution kolme akselia vastaavat kolmea erilaista lisäystä yksinkertaisesti kirjoitettuun lambda-laskentaan: riippuvien tyyppien lisääminen, polymorfismin lisääminen ja korkeamman asteen tyyppisten konstruktorien lisääminen.

Muodollinen määritelmä

Hyvin yksinkertaistetusti riippuvainen tyyppi voidaan ajatella indeksoidun joukkojen perheen tyyppinä. Muodollisemmin tyypille (missä on tyyppien universumi) voit määrittää tyyppiperheen , joka kartoittaa jokaisen termin tyyppiin , joka kirjoitetaan nimellä . Funktiota, jonka alue vaihtelee argumentin mukaan, kutsutaan riippuvaiseksi funktioksi . Tämän funktion tyyppiä kutsutaan riippuvaisen tyypin tuloksi , pi-tyypiksi tai yksinkertaisesti riippuvaiseksi tyypiksi . Riippuva tyyppi on kirjoitettu tässä tapauksessa muodossa $V:{\mathcal {U}}$ ${\mathcal {U}}$ $B$ $a:A$ $B(a):{\mathcal {U}}$ $B:A\to {\mathcal {U}}$

\Pi _{{(x:A)}}B(x)

tai

\Pi(x:A),B(x)

Jos on vakio, niin riippuvainen tyyppi yksinkertaistuu normaaliksi funktioksi . Toisin sanoen se vastaa funktiotyyppiä . Nimi " pi-tyyppi " korostaa, että tällainen tyyppi on tyyppien karteesinen tulo . Pi - tyyppejä voidaan esittää myös universaaleina kvantorimalleina . $B$ $A:sta B:hen$ $\Pi _{{(x:A)}}B$ $A:sta B:hen$

Esimerkiksi, jos on reaalilukujen monikko , niin on funktioiden tyyppi, joka mille tahansa luonnolliselle luvulle palauttaa joukon reaalilukuja, joiden koko on . Tavallinen funktioavaruus on erikoistapaus, jossa alue ei riipu syöteparametrista: esimerkiksi - funktioiden tyyppi luonnollisesta todelliseen, ilmaistaan yksinkertaisesti kirjoitetussa lambda-laskennassa . ${\mbox{Vec}}({{\mathbb R}},n)$ $n$ $\Pi _{{(n:{{\mathbb N}})))}{\mbox{Vec}}({{\mathbb R}}),n)$ $n$ $n$ $\Pi _{{(n:{{\mathbb N}})))}\;{{\mathbb R}}$ ${{\mathbb N}}\to {{\mathbb R}}$

Polymorfiset funktiot ovat tärkeä esimerkki riippuvaisista funktioista, eli funktioista, joilla on riippuvainen tyyppi. Jollekin tietylle tyypille tällaiset funktiot toimivat kyseisen tyypin arvoilla tai kyseisestä tyypistä johdetuilla arvoilla. Tyypin arvoja palauttavan polymorfisen funktionpolymorfinen tyyppi on kirjoitettu muodossa $C$

\Pi _{{(A:{\mathcal {U))))}A\-C

Kirjallisuus

Chlipala, A. Sertifioitu ohjelmointi riippuvaisilla tyypeillä: käytännöllinen johdatus Coq Proof Assistantiin . - MIT Press, 2013. - 440 s. — ISBN 9780262026659 . ( teksti tekijän verkkosivuilta (eng.) )
Jeremy Paul Condit. Turvallisten järjestelmien ohjelmistojen riippuvat tyypit. - Väitöskirja. – Kalifornian yliopisto Berkeleyssä, 2007.