Agda

Kokeneet kirjoittajat eivät ole vielä tarkistaneet sivun nykyistä versiota, ja se voi poiketa merkittävästi 21. huhtikuuta 2021 tarkistetusta versiosta . tarkastukset vaativat 3 muokkausta .
Agda
Kieliluokka toiminnallinen , lauseen todistaja
Esiintyi 2007 (1,0 vuonna 1999 ) ( 2007 ) ( 1999 )
Tekijä Ulf Norell
Tiedostotunniste _ .agdatai.lagda
Vapauta 2.6.2.2 (2. huhtikuuta 2022 ) ( 2022-04-02 )
Tyyppijärjestelmä staattinen , tiukka , riippuvainen
Vaikutettu Haskell , Coq , Epigram
vaikutti Idris
Lisenssi BSD
Verkkosivusto wiki.portal.chalmers.se/…
OS Microsoft Windows ja Unix kaltainen käyttöjärjestelmä

Agda  on puhdas toiminnallinen ohjelmointikieli , jossa on riippuvaisia ​​tyyppejä , eli tyyppejä, jotka voidaan indeksoida toisen tyypin arvoilla. Agdan teoreettinen perusta on Martin-Löfin intuitionistinen tyyppiteoria , jota laajennetaan käytännön ohjelmoinnin kannalta hyödyllisillä konstruktioilla.

Agda on myös automaattinen todistusjärjestelmä . Loogiset lauseet kirjoitetaan tyypeinä ja todistukset ovat vastaavan tyyppisiä ohjelmia.

Agda tukee induktiivisia tietotyyppejä, kuvioiden täsmäämistä (joustavasti käyttämällä riippuvaisten tyyppien läsnäoloa), parametroitujen moduulien järjestelmää, ohjelman lopettamisen tarkistusta, mixfix syntaksi operaattoreille. Implisiittisten argumenttien tuki yksinkertaistaa huomattavasti ohjelmointia riippuvaisilla tyypeillä. Agda-ohjelmille on ominaista Unicoden laaja käyttö .

Agdan vakiototeutus sisältää laajennuksen Emacs -editoriin , jonka avulla voit rakentaa ohjelmia askel askeleelta. Kielen tyyppitarkistusjärjestelmä antaa ohjelmoijalle hyödyllistä tietoa ohjelman osista, joita ei ole vielä kirjoitettu.

Agda-kielen erityinen syntaksi on hyvin lähellä Haskellin syntaksia , johon Agda-järjestelmä on toteutettu.

Esimerkkejä

Luonnolliset luvut ja niiden yhteenlasku

data Nat : Aseta missä nolla : Nat suc : Nat -> Nat _+_ : Nat -> Nat -> Nat nolla + m = m suc n + m = suc ( n + m )

Esimerkki riippuvaisesta tyypistä: lista, jonka tyyppi tallentaa luonnollisen luvun - sen pituuden

data Vec ( A : Set ) : Nat -> Aseta missä [] : Vec A nolla _::_ : { n : Nat } -> A -> Vec A n -> Vec A ( suc n )

Turvallinen listapään laskentatoiminto, joka ei salli tämän toiminnon suorittamista tyhjälle listalle (nollapituus):

head : { A : Set }{ n : Nat } -> Vec A ( suc n ) -> A pää ( x :: xs ) = x

Muistiinpanot

Linkit

 Ohjelmointikielet