| Agda | |
|---|---|
| Jazyková třída | funkční , dokaz věty |
| Objevil se v | 2007 (1,0 v roce 1999 ) |
| Autor | Ulf Norell |
| Přípona souboru | .agdanebo.lagda |
| Uvolnění | 2.6.2.2 (2. dubna 2022 ) |
| Typový systém | statický , přísný , závislý |
| Byl ovlivněn | Haskell , Coq , Epigram |
| ovlivnil | Idris |
| Licence | BSD |
| webová stránka | wiki.portal.chalmers.se/… |
| OS | Microsoft Windows a operační systém podobný Unixu |
Agda je čistý funkcionální programovací jazyk se závislými typy , tedy typy, které lze indexovat hodnotami jiného typu. Teoretickým základem Agdy je Martin-Löfova intuicionistická teorie typů , která je rozšířena o sadu konstrukcí užitečných pro praktické programování.
Agda je také automatický kontrolní systém . Logické výroky jsou psány jako typy a důkazy jsou programy odpovídajícího typu.
Agda podporuje indukční datové typy, porovnávání vzorů (flexibilně využívající přítomnost závislých typů), systém parametrizovaných modulů, kontrolu ukončení programu, mixfix syntaxe pro operátory. Podpora implicitních argumentů značně zjednodušuje programování se závislými typy. Programy Agda se vyznačují rozšířeným používáním Unicode .
Standardní implementace Agda obsahuje rozšíření editoru Emacs , které vám umožňuje vytvářet programy krok za krokem. Systém kontroly typu jazyka poskytuje programátorovi užitečné informace o částech programu, které ještě nebyly napsány.
Specifická syntaxe jazyka Agda je velmi blízká syntaxi Haskell , na které je implementován systém Agda.
Přirozená čísla a jejich sčítání
data Nat : Nastavit kde nula : Nat suc : Nat -> Nat _+_ : Nat -> Nat -> Nat nula + m = m suc n + m = suc ( n + m )Příklad závislého typu: seznam, jehož typ ukládá přirozené číslo - jeho délku
data Vec ( A : Set ) : Nat -> Set kde [] : Vec A nula _::_ : { n : Nat } -> A -> Vec A n -> Vec A ( suc n )Funkce bezpečného výpočtu hlavy seznamu, která neumožňuje provedení této operace na prázdném seznamu (nulová délka):
hlava : { A : Set }{ n : Nat } -> Vec A ( suc n ) -> A hlava ( x :: xs ) = x| Programovací jazyky | |
|---|---|
| |