| Idris | |
|---|---|
| Kieliluokka | Toimiva |
| Esiintyi | 2007 [3] [4] [5] |
| Tekijä | Edwin Brady |
| Tiedostotunniste _ | .idrtai.lidr |
| Vapauta | Idris 2 -versio 0.5.1 [1] (20. syyskuuta 2021 ) |
| Tyyppijärjestelmä | tiukka , staattinen , riippuvainen tyyppituki |
| Vaikutettu | Agda , Coq , [2] Epigram , Haskell , [2] ML , [2] Rust |
| Lisenssi | BSD-3 |
| Verkkosivusto | idris-lang.org |
Idris on puhdas , täydellinen toiminnallinen yleiskäyttöinen ohjelmointikieli, jossa on Haskellin kaltainen syntaksi ja tuki riippuville tyypeille [6] . Tyyppijärjestelmä on samanlainen kuin Agda - tyyppijärjestelmä .
Kieli tukee Coqiin verrattavia automaattisia oikolukuja , mukaan lukien tuki taktiikalle, mutta ei keskity niihin, vaan se on sijoitettu yleiskäyttöiseksi ohjelmointikieleksi . Sen luomisen tavoitteet: "riittävä" suorituskyky, sivuvaikutusten hallinnan helppous ja keinot upotettavien verkkotunnuskohtaisten kielten toteuttamiseen .
Toteutettu Haskellissa , saatavana Hackage- pakettina [7] . Idris-lähdekoodi kootaan joukoksi väliesityksiä [8] ja niistä C - koodiksi, joka suoritetaan käyttämällä Cheney -algoritmia kopiojätteenkerääjällä . Myös virallisesti toteutettu kyky kääntää JavaScript -koodiksi (mukaan lukien Node.js ). On olemassa kolmansien osapuolien koodigeneraattoreita Javalle , JVM :lle , CIL :lle , Erlangille , PHP :lle ja (rajoitetusti) LLVM :lle .
Kieli on nimetty laulavan lohikäärme Idrisin mukaan vuoden 1970 brittiläisestä lasten TV-ohjelmasta Ivor the Tank Engine [9] .
Kielessä yhdistyvät suosituimpien toiminnallisten ohjelmointikielten ominaisuudet automaattisista todistejärjestelmistä lainattuihin ominaisuuksiin, mikä hämärtää tehokkaasti kahden kieliluokan välistä rajaa.
Kielen toinen versio (julkaistu vuonna 2020, perustuu "kvantitatiiviseen tyyppiteoriaan" [10] ) eroaa merkittävästi ensimmäisestä: täysi tuki lineaarisille tyypeille on lisätty , koodi käännetään oletuksena Scheme , kielen kääntäjä on kirjoitettu itse kielellä .
Kielen syntaksi (kuten Agdan syntaksi ) on lähellä Haskellin syntaksia [11] . Hei maailma! Idriksessä näyttää tältä:
moduuli Main main : IO () main = putStrLn "Hei, maailma!"Erot tämän ohjelman ja sen Haskell-vastineen välillä ovat yksi (kaksoispiste) kaksoispiste pääfunktion allekirjoituksessa ja "jos"-sanan puuttuminen moduulin määrittelystä.
Kuten useimmat nykyaikaiset toiminnalliset ohjelmointikielet, kieli tukee rekursiivisia (induktion määrittelemiä) tietotyyppejä ja parametrista polymorfismia . Tällaiset tyypit voidaan määritellä kuten perinteisessä "Haskell98"-syntaksissa:
data Puu a = Solmu ( Puu a ) ( Puu a ) | lehti aja yleisemmässä GADT- syntaksissa:
data Puu : Tyyppi -> Kirjoita missä Solmu : Puu a -> Puu a -> Puu a Lehti : a -> Puu aRiippuvien tyyppien avulla on mahdollista tyyppitarkistuksen vaiheessa suorittaa laskelmia, jotka sisältävät tyyppejä parametroivia arvoja. Seuraava koodi määrittelee listan, jolla on staattisesti annettu pituus, jota kutsutaan perinteisesti vektoriksi :
tiedot Vect : Nat -> Tyyppi -> Tyyppi jossa Nolla : Vect 0 a (::) : ( x : a ) -> ( xs : Vect na ) -> Vect ( n + 1 ) aTätä tyyppiä voidaan käyttää seuraavasti:
yhteensä liite : Vect na -> Vect ma -> Vect ( n + m ) a liitä Nil ys = ys liitä ( x :: xs ) ys = x :: liitä xs ysFunktio liittää tyyppielementtien vektorin mtyyppielementtien avektoriin . Koska syöttövektoreiden tarkka tyyppi riippuu arvoista, jotka ovat varmasti tiedossa käännöshetkellä, tuloksena oleva vektori sisältää täsmälleen tyypin elementtejä . na(n + m)a
Sana " total" vaatii jäsentämisen täydellisyyden tarkistuksen :tä vastaan , joka, jotta vältytään päättymättömästä silmukasta , ilmoittaa virheestä, jos funktio ei kata kaikkia mahdollisia -tapauksia tai sitä ei voida (automaattisesti) todistaa.
Toinen esimerkki: kahden pituuden mukaan parametroidun vektorin pareittainen lisääminen:
pari yhteensä Lisää : Num a => Vanha na -> Vanha na -> Vect na pariLisäys Nolla Nolla = Ei pariLisää ( x :: xs ) ( y :: ys ) = x + y :: pariLisää xs ysNumtarkoittaa, että tyyppi akuuluu tyyppiluokkaan Num . Funktio läpäisee tyyppitarkistuksen. Tapausta, jossa yhden vektorin arvo on Nolla, kun taas toinen on luku, ei voi tapahtua. Tyyppijärjestelmä tarkistaa käännöshetkellä, että molempien vektoreiden pituus täsmää. Tämä yksinkertaistaa funktion tekstiä, jota ei enää tarvita tämän erikoistapauksen käsittelemiseksi.
Riippuvat tyypit ovat tarpeeksi tehokkaita kuvaamaan useimpia ohjelmien ominaisuuksia, joten Idris-ohjelma voi todistaa invariantteja käännöshetkellä. Tämä muuttaa kielen interaktiiviseksi todistejärjestelmäksi .
Idris tukee kahta tapaa työskennellä automaattisen todistusjärjestelmän kanssa: kirjoittamalla peräkkäisiä taktiikkakutsuja ( Coq -tyyli , kun taas käytettävissä olevien taktiikkojen joukko ei ole yhtä runsas kuin Coqissa, mutta sitä voidaan laajentaa tavallisilla metaohjelmointityökaluilla ) tai vaiheittain -askelvarma kehitys ( Epigram ja Agda tyyli ).