Agda

Appeared in:
1999
Influenced by:
Paradigm:
Typing discipline:
File extensions:
.agda, .lagda
Versions and implementations (Collapse all | Expand all):
Programming language

Agda is both a functional dependently-typed programming language and a proof assistant. It is developed at Chalmers University of Technology as a successor of older proof assistants.

The language is based on a constructive type theory á la Martin-Löf, extended with dependent record types, inductive definitions, module structures and a class hierarchy mechanism. The class mechanism of Agda is similar to that of Haskell.

The language has evolved through several significantly different stages. The oldest version, referred to as Agda1/OldSyntax, was created in 1999 and is not available any more. It was followed by Agda1/NewSyntax, available since 2005. Current version is Agda 2.

Elements of syntax:

Inline comments --
Nestable comments {- ... -}

Links:

Examples:

Hello, World!:

Example for versions agda 2.2.6

Just writing strings is not a natural task for Agda, so it needs some extra installations.

This example should be saved in file “helloworld.agda”. You’ll have to install agda standard library (agda-stdlib); this was tested with agda 2.2.6 and agda-stdlib 0.3. To compile the example, use agda -i [library path] -i . -c helloworld.agda, where [library path] is a path to where you installed agda-stdlib. This compiles Agda source code into Haskell code, and then converts it into an executable. 

module helloworld where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Data.Char using (Char)
open import Foreign.Haskell using (fromColist; Colist; Unit)
open import Data.Function

fromString = fromColist . toCostring

main : IO Unit
main = putStrLn (fromString "Hello, World!")