| Agda | |
|---|---|
| Sprog klasse | funktionel , sætningsbevis |
| Dukkede op i | 2007 (1,0 i 1999 ) |
| Forfatter | Ulf Norell |
| Filtypenavn _ | .agdaeller.lagda |
| Frigøre | 2.6.2.2 (2. april 2022 ) |
| Type system | statisk , streng , afhængig |
| Blev påvirket | Haskell , Coq , Epigram |
| påvirket | Idris |
| Licens | BSD |
| Internet side | wiki.portal.chalmers.se/… |
| OS | Microsoft Windows og Unix-lignende operativsystem |
Agda er et rent funktionelt programmeringssprog med afhængige typer , det vil sige typer, der kan indekseres med værdier af en anden type. Det teoretiske grundlag for Agda er Martin-Löfs intuitionistiske typeteori , som er udvidet med et sæt konstruktioner, der er nyttige til praktisk programmering.
Agda er også et automatisk bevissystem . Logiske påstande skrives som typer, og beviser er programmer af den tilsvarende type.
Agda understøtter induktive datatyper, mønstertilpasning (fleksibelt ved hjælp af tilstedeværelsen af afhængige typer), et system af parametriserede moduler, kontrol af programafslutning, mixfix-syntaks for operatører. Understøttelse af implicitte argumenter forenkler i høj grad programmering med afhængige typer. Agda-programmer er kendetegnet ved den udbredte brug af Unicode .
Standardimplementeringen af Agda inkluderer en udvidelse til Emacs- editoren , der giver dig mulighed for at bygge programmer trin for trin. Sprogets typekontrolsystem giver programmøren nyttig information om dele af programmet, som endnu ikke er skrevet.
Den specifikke syntaks for Agda-sproget er meget tæt på syntaksen for Haskell , som Agda-systemet er implementeret på.
Naturlige tal og deres addition
data Nat : Indstil hvor nul : Nat suc : Nat -> Nat _+_ : Nat -> Nat -> Nat nul + m = m suc n + m = suc ( n + m )Eksempel på en afhængig type: en liste, hvis type gemmer et naturligt tal - dets længde
data Vec ( A : Sæt ) : Nat -> Indstil hvor [] : Vec A nul _::_ : { n : Nat } -> A -> Vec A n -> Vec A ( suc n )En sikker listehovedberegningsfunktion, der ikke tillader denne operation at blive udført på en tom liste (nul længde):
hoved : { A : Sæt }{ n : Nat } -> Vec A ( suc n ) -> A hoved ( x :: xs ) = x| Programmeringssprog | |
|---|---|
| |