| Agda | |
|---|---|
| clase de idioma | probador de teoremas funcional |
| Apareció en | 2007 (1.0 en 1999 ) |
| Autor | ulf norell |
| extensión de archivo | .agdao.lagda |
| Liberar | 2.6.2.2 (2 de abril de 2022 ) |
| sistema de tipos | estático , estricto , dependiente |
| sido influenciado | Haskell , Coq , Epigrama |
| influenciado | Idris |
| Licencia | BSD |
| Sitio web | wiki.portal.chalmers.se/… |
| sistema operativo | Sistema operativo similar a Microsoft Windows y Unix |
Agda es un lenguaje de programación funcional puro con tipos dependientes , es decir, tipos que pueden ser indexados por valores de otro tipo. La base teórica de Agda es la teoría de tipo intuicionista de Martin-Löf , que se amplía con un conjunto de construcciones útiles para la programación práctica.
Agda es también un sistema de prueba automático . Las proposiciones lógicas se escriben como tipos y las demostraciones son programas del tipo correspondiente.
Agda admite tipos de datos inductivos, coincidencia de patrones (utilizando de manera flexible la presencia de tipos dependientes), un sistema de módulos parametrizados, verificación de terminación de programa, sintaxis mixfix para operadores. La compatibilidad con argumentos implícitos simplifica enormemente la programación con tipos dependientes. Los programas de Agda se caracterizan por el uso generalizado de Unicode .
La implementación estándar de Agda incluye una extensión del editor de Emacs que le permite crear programas paso a paso. El sistema de verificación de tipos del lenguaje brinda al programador información útil sobre partes del programa que aún no se han escrito.
La sintaxis específica del lenguaje Agda es muy parecida a la sintaxis de Haskell , sobre la que se implementa el sistema Agda.
Números naturales y su suma.
data Nat : Establecer donde cero : Nat suc : Nat -> Nat _+_ : Nacional -> Nacional -> Nacional cero + metro = metro suc norte + metro = suc ( norte + metro )Ejemplo de un tipo dependiente: una lista cuyo tipo almacena un número natural - su longitud
data Vec ( A : Set ) : Nat -> Set where [] : Vec A zero _::_ : { n : Nat } -> A -> Vec A n -> Vec A ( suc n )Una función de cálculo de encabezado de lista segura que no permite realizar esta operación en una lista vacía (longitud cero):
head : { A : Set }{ n : Nat } -> Vec A ( suc n ) -> A cabeza ( x :: xs ) = x| Lenguajes de programación | |
|---|---|
| |