Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Agda (programming language)
Résumé
Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.
Agda is also a proof assistant based on the propositions-as-types paradigm, but unlike Coq, has no separate tactics language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. The system has Emacs, Atom, and VS Code interfaces but can also be run in batch mode from the command line.
Agda is based on Zhaohui Luo's unified theory of dependent types (UTT), a type theory similar to Martin-Löf type theory.
Agda is named after the Swedish song "Hönan Agda", written by Cornelis Vreeswijk, which is about a hen named Agda. This alludes to the name of the theorem prover Coq, which was named after Thierry Coquand, Catarina Coquand's husband.
The main way of defining data types in Agda is via inductive data types which are similar to algebraic data types in non-dependently typed programming languages.
Here is a definition of Peano numbers in Agda:
data N : Set where
zero : N
suc : N → N
Basically, it means that there are two ways to construct a value of type , representing a natural number. To begin, zero is a natural number, and if n is a natural number, then suc n, standing for the successor of n, is a natural number too.
Here is a definition of the "less than or equal" relation between two natural numbers:
data ≤ : N → N → Set where
z≤n : {n : N} → zero ≤ n
s≤s : {n m : N} → n ≤ m → suc n ≤ suc m
The first constructor, z≤n, corresponds to the axiom that zero is less than or equal to any natural number. The second constructor, s≤s, corresponds to an inference rule, allowing to turn a proof of n ≤ m into a proof of suc n ≤ suc m.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.