Annotations about Agda

Agda-annotations.md

Agda is a dependently typed functional programming. Dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value.

• A dependent function's return type may depend on the value (not just type) of an argument. A function that takes a positive integer "n" may return an array of length "n".

• A dependent pair may have a second value that depends on the first. It can be used to encode a pair of integers where the second one is greater than the first.

  A definition is a syntactic construction defining an entity such as a function or a datatype.

  f : (x : A) → B is a dependently typed function, i.e. x can occur in B.

  When B does not depend on x we write f : A → B

  Example: If Fin n is the set of all natural numbers less than n, then a : (n : N) → Fin (n + 1) is a sequence such that a(mini n) < n + 1

Using Agda on Atom - Keys combination

• C-c stands for "press Ctrl and c at the same time"
• When it comes to combos like C-c C-l, you can often slur them into "hold Ctrl while pressing c and then l"

It is necessary to have spaces between most lexical units.

data tells us this is an inductive definition, that is, that we are defining a new datatype with constructors.

set is the way in Agda of saying that it is a type.

{-# BUILTIN NATURAL Nat #-} shorthand to tell that something represent the natural numbers

Operations on Naturals

• Application has precedence over any operator.

  suc m + n to mean (suc m) + n

• Multiplication has precedence over addition

• Sometimes is said that addition associates to the left.

  m + n + p to mean (m + n) + p.

infixl indicates that the operator associate to the left

6 indicates the value of precedence

infixl 6  _+_  _∸_
infixl 7  _*_

infixr indicates that operator associate to the right

Properties of operators

• Identity. Operator + has left identity 0 if 0 + n ≡ n, and right identity 0 if n + 0 ≡ n, for all n. A value that is both a left and right identity is just called an identity. Identity is also sometimes called unit.
• Associativity. Operator + is associative if the location of parentheses does not matter: (m + n) + p ≡ m + (n + p), for all m, n, and p.
• Commutativity. Operator + is commutative if order of arguments does not matter: m + n ≡ n + m, for all m and n.
• Distributivity. Operator * distributes over operator + from the left if (m + n) * p ≡ (m * p) + (n * p), for all m, n, and p, and from the right if m * (p + q) ≡ (m * p) + (m * q), for all m, p, and q.

The base case tells us that (zero + n) + p ≡ zero + (n + p) for every natural n and p. The inductive case tells us that if (m + n) + p ≡ m + (n + p) (on the day before today) then (suc m + n) + p ≡ suc m + (n + p) (today)

refl: The proof that a term is equal to itself

rewrite:

postulate plus-commute : (a b : Nat) → a + b ≡ b + a

thm : (a b : Nat) → P (a + b) → P (b + a)
thm a b t with   a + b  | plus-commute a b
thm a b t    | .(b + a) | refl = t

This pattern of rewriting by an equation by with-abstracting over it and its left-hand side is common enough that there is special syntax for it:

thm : (a b : Nat) → P (a + b) → P (b + a)
thm a b t rewrite plus-commute a b = t

The rewrite construction takes a term eq of type lhs ≡ rhs, where _≡_ is the built-in equality type, and expands to a with-abstraction of lhs and eq followed by a match of the result of eqagainst refl:

---

Talking a little about lambda calculus

x : A 􏰀 x describes a deduction of A

id : (A : P) → A → A
id = λA → λx → x

Resources

Keys usage for Atom

agda-mode

Example of Agda program

agda/agda

https://en.wikipedia.org/wiki/Dependent_type