Rapid explanation of Agda

• Syntax and concepts
• Sugar

A precursor of Agda was CHalf, now obsolete.

Agda is written in haskell and emacs lisp, and is quite easy to use. The editing interface is a standard emacs mode, which is a front end for a line mode interpreter. It is a simple and elegant tool for carefully working out definitions and constructive proofs.

Thomas Hallgren in Chalmers has written an editing GUI called alfa, which provides an alternative, sexier environment for proof editing. It also is quite easy to use, though it requires a powerful machine.

There are other developments connected with Agda; eg. seemingly something written by Aarne Ranta that will translate proofs into ordinary natural languages.

Syntax and concepts

In Agda one has:

Functions

functional types:

(x :: A)-> B

abstraction form:

\ (x :: A)-> b

application form:

b a

Named products

product form:

sig { x1 :: A1; .. }

tuple form:

struct { x1=a1; .. }

selection form:

a.xi

These let you chunk-up blocks of formal material, and refer to chunk components by name. Note: the blocks can be empty, as in sig{},struct{}.

Named sums

sum form:

data { x1 ( y1 : A1, .. , yk : Ak ) | .. } . Here the xi are constructor names, that live in a name space specific to each instance of the type. Constructors are disambiguated as follows xi@type.

constructor form:

x1 a1 .. ak

case form:

case a of { (x1 y1 .. yk) -> a1 ; .. }

Facilities for tagging data with named constructors. Note: there can be zero tags data{}; and a given tag may have no data data{..,$xi,..}. The behaviour of constructors with respect to type-checking is extremely subtle. They exhibit a kind of polymorphism; they are not functions.

Lets

let { x1 :: A1 = a1, .. } in a

Definitions can be mutually recursive.

Sets, Types, Kind, Packages

Set : Type : Kind, Theory : Kind

Set, Type, and Kind are (predicatively) closed under the above constructions.

Packages are named collections of definitions whose definitions take the form package name params where { x1 = a1 : A1, .. } , and the definitions within them may be selected by name as with tuples. Packages are supplemented with a lot of useful sugar, which I havent got time to describe just now.

Sugar

There is a certain amount of extra sugar that goes with these. Here is some (I may have forgotten something).

layout

Very usefull: one can use layout (indentation) instead of syntactical noise like braces, semicolons, etc.

Infix operators

A name may be used as an infix operator, by enclosing it in back-quotes, as in `foo`.

Symbolic operators

I haven't mastered these.

repeated abstraction form:

\ (x,y::A) -> a is sugar for \ (x :: A) -> \ (y :: A) -> a .

repeated functional form:

( x, y : A, .. ) -> a is sugar for ( x :: A ) -> (y :: A)-> .. -> a .

left hand side parameters:

f ( x1 :: A1, .. ) :: A = a is sugar for f = (x1 :: A1) -> .. A = \ (x1 :: A1) .. -> a : ( x1 : A1, .. )-> A

use of `useless variables'

In ( x : A )-> B, the variable x need'nt occur in B. It's a drag to think of a name. Instead, one may use (in binding position) the identifier "_", as in Haskell. This usually helps to make the code clearer. If a name is supplied it is used by the proof editor as a default, when one sends the checker an Intro command. Furthermore, there's the familar abbreviation A -> B of (_ :: A) -> B.

Nestable comments in Agda are like this {- .. -}. One line comments (to end of line) are introduced by --.

Files may be included with special comments

--#include "file.name"

Unfinished bits are represented like this: {! text !} or ?.

Sometime I might try to describe what it is the type-checker does.