Agda es un lenguaje de programación funcional de tipado dependiente desarrollado originalmente por Ulf Norell en la Universidad Tecnológica de Chalmers con una implementación descrita en su tesis doctoral. [2] El sistema Agda original fue desarrollado en Chalmers por Catarina Coquand en 1999. [3] La versión actual, originalmente llamada Agda 2, es una reescritura completa, que debe considerarse un nuevo lenguaje que comparte un nombre y una tradición.
Agda también es un asistente de pruebas basado en el paradigma de proposiciones como tipos ( correspondencia de Curry-Howard ), pero a diferencia de Coq , no tiene un lenguaje de tácticas separado y las pruebas se escriben en un estilo de programación funcional. El lenguaje tiene construcciones de programación ordinarias como tipos de datos , coincidencia de patrones , registros , expresiones let y módulos, y una sintaxis similar a Haskell . El sistema tiene interfaces Emacs , Atom y VS Code [4] [5] [6] pero también se puede ejecutar en modo de procesamiento por lotes desde una interfaz de línea de comandos .
Agda se basa en la teoría unificada de tipos dependientes (UTT) de Zhaohui Luo, [7] una teoría de tipos similar a la teoría de tipos de Martin-Löf .
Agda recibe su nombre de la canción sueca "Hönan Agda", escrita por Cornelis Vreeswijk , [8] que trata sobre una gallina llamada Agda. Esto alude al nombre del demostrador de teoremas Coq , que recibió su nombre en honor a Thierry Coquand .
La forma principal de definir tipos de datos en Agda es a través de tipos de datos inductivos que son similares a los tipos de datos algebraicos en lenguajes de programación no dependientes del tipo.
Aquí hay una definición de los números de Peano en Agda:
datos ℕ : Conjunto donde cero : ℕ suc : ℕ → ℕ Básicamente, significa que hay dos formas de construir un valor de tipo , que representa un número natural. Para empezar, es un número natural, y si es un número natural, entonces , que representa al sucesor de , también es un número natural.zeronsuc nn
Aquí hay una definición de la relación "menor o igual" entre dos números naturales:
datos _≤_ : ℕ → ℕ → Conjunto donde z≤n : { n : ℕ } → cero ≤ n s≤s : { n m : ℕ } → n ≤ m → suc n ≤ suc m El primer constructor, z≤n, corresponde al axioma de que cero es menor o igual que cualquier número natural. El segundo constructor, s≤s, corresponde a una regla de inferencia, que permite convertir una prueba de n ≤ men una prueba de suc n ≤ suc m. [9] Por lo tanto, el valor s≤s {zero} {suc zero} (z≤n {suc zero})es una prueba de que uno (el sucesor de cero), es menor o igual que dos (el sucesor de uno). Los parámetros proporcionados entre llaves se pueden omitir si se pueden inferir.
En la teoría de tipos básicos, se utilizan los principios de inducción y recursión para demostrar teoremas sobre tipos inductivos . En Agda, se utiliza en cambio la comparación de patrones con tipos dependientes. Por ejemplo, la suma de números naturales se puede definir de la siguiente manera:
suma cero n = n suma ( suc m ) n = suc ( suma m n ) Esta forma de escribir funciones recursivas o pruebas inductivas es más natural que aplicar principios de inducción puros. En Agda, la comparación de patrones con tipos dependientes es un elemento primitivo del lenguaje; el lenguaje central carece de los principios de inducción o recursión a los que se traduce la comparación de patrones.
Una de las características distintivas de Agda, en comparación con otros sistemas similares como Coq , es su gran dependencia de metavariables para la construcción de programas. Por ejemplo, en Agda se pueden escribir funciones como esta:
suma : ℕ → ℕ → ℕ suma x y = ? ?Aquí hay una metavariable. Al interactuar con el sistema en modo emacs, le mostrará al usuario el tipo esperado y le permitirá refinar la metavariable, es decir, reemplazarla con código más detallado. Esta característica permite la construcción incremental de programas de una manera similar a los asistentes de prueba basados en tácticas como Coq.
La programación en teoría de tipos pura implica muchas pruebas tediosas y repetitivas. Aunque Agda no tiene un lenguaje de tácticas independiente, es posible programar tácticas útiles dentro de Agda. Por lo general, esto funciona escribiendo una función de Agda que, opcionalmente, devuelve una prueba de alguna propiedad de interés. Luego, se construye una táctica ejecutando esta función en el momento de la verificación de tipos, por ejemplo, utilizando las siguientes definiciones auxiliares:
datos Quizás ( A : Conjunto ) : Conjunto donde Sólo : A → Quizás A Nada : Quizás A data isJust { A : Set } : Maybe A → Set donde auto : ∀ { x } → isJust ( Solo x ) Táctica : ∀ { A : Establecer } ( x : Quizás A ) → esSolo x → A Táctica Nada () Táctica ( Solo x ) auto = x Dada una función que ingresa un número y opcionalmente devuelve una prueba de su paridad, se puede construir una táctica de la siguiente manera:check-even : (n : ) → Maybe (Even n)
check-even-tactic : { n : ℕ } → isJust ( check-even n ) → Even n check-even-tactic { n } = Tactic ( check-even n ) lema0 : cero par lema0 = check-even-tactic auto lema2 : Even ( suc ( suc cero )) lema2 = check-even-tactic auto La prueba real de cada lema se construirá automáticamente en el momento de la verificación de tipos. Si la táctica falla, la verificación de tipos fallará.
Además, para escribir tácticas más complejas, Agda admite la automatización a través de la programación reflexiva (reflexión). El mecanismo de reflexión permite citar fragmentos de programa en el árbol de sintaxis abstracta o quitarles las citas del mismo. La forma en que se utiliza la reflexión es similar a la forma en que funciona Template Haskell . [10]
Otro mecanismo para la automatización de pruebas es la acción de búsqueda de pruebas en modo Emacs . Enumera los términos de prueba posibles (limitados a 5 segundos) y, si uno de los términos se ajusta a la especificación, se colocará en la variable meta donde se invoca la acción. Esta acción acepta sugerencias, por ejemplo, qué teoremas y de qué módulos se pueden utilizar, si la acción puede utilizar la coincidencia de patrones, etc. [11]
Agda es un lenguaje de programación totalmente funcional , es decir, cada programa que lo compone debe terminar y todos los patrones posibles deben coincidir. Sin esta característica, la lógica detrás del lenguaje se vuelve inconsistente y se hace posible probar afirmaciones arbitrarias. Para la comprobación de terminaciones , Agda utiliza el enfoque del verificador de terminaciones Foetus. [12]
Agda cuenta con una extensa biblioteca estándar de facto , que incluye muchas definiciones y teoremas útiles sobre estructuras de datos básicas, como números naturales, listas y vectores. La biblioteca se encuentra en fase beta y se encuentra en desarrollo activo.
Una de las características más notables de Agda es su gran dependencia de Unicode en el código fuente del programa. El modo estándar de emacs utiliza atajos para la entrada, como \SigmaΣ.
Hay dos backends de compilación, MAlonzo para Haskell y uno para JavaScript .