# [Agda] beginner questions

Serge D. Mechveliani mechvel at botik.ru
Mon Jul 23 14:04:41 CEST 2012

```People,
I have the following beginner questions.

(1) The example program
Agda-2.3.0.1/examples/instance-arguments/06-listEquality.agda
ends with

test = eq (true :: false :: true :: []) (true :: false :: [])
where listBoolEq = listEq eqBool

And I do not understand these two lines.
Should it be
test = (listEq eqBool).eq
(true :: false :: true :: []) (true :: false :: [])
?

(2) Do there exist papers (manustripts, descriptions, explanation) about
the Standard Library (somewhat its principles, architecture etc.) ?

(3) tutorial.pdf  for Agda often writes  T : Set,
while Standard Library writes        T : Set a,
where I expect `a' to be a type parameter. So, `small' types look like
being parameterized by a type `a'.
Some small comment is nedeed.
Does this mean that  T  is any `small' subtype in a type `a' ?

(4) Instances in the Standard Library.
The Standard Library lib-0.6 provides the `classes' (records) for
Semigroup, Group, ..., Ring.
Does it also provide some classical instances for them?
For example,
* the instances up to  CommutativeRing  for  Integer
(CommutativeSemigroup, CommutativeGroup  for  +,
CommutativeSemigroup, CommutativeMonoid for  *,
distributivity, CommutativeRing
),

* the instance (record map)
(Ring A, Ring B) => Ring (A, B) where  -- coordinatewise operations
-- in the direct product A x B
How could these instances (record maps) look?

(5) On the practice of dependent type programming
(sorry for a naive question!).

tutorial.pdf  for Agda writes in  Chapter 2.5 "Programs as proofs"

lookup : {A : Set}(xs : List A)(n : Nat) ->
isTrue (n < length xs) -> A
lookup []        n       ()
lookup (x :: xs) zero    p  = x
lookup (x :: xs) (suc n) p  = lookup xs n p

What is its expected usage on practice?
For, example, "the 20-th element in the charater list  ['a' .. 'z']"
(the segment from 'a' to 'z')" :

lookup ['a' .. 'z'] 19' p    -- 19' abbreviates 19 in the unary system.

What does one need to put for  p
(of the type  isTrue (19' < length ['a' .. 'z'])
?
Must it be any `proof' of the statement  (19' < length ['a' .. 'z'])  ?
And where does one take such a proof? Has one to write

lookup ['a' .. 'z'] 19' p   where
p = if 19' < length ['a' .. 'z'] then
trivial : True
else  ()  -- ?
?

Thank you in advance for explanation,

------
Sergei
mechvel at botik.ru
```