[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
More information about the Agda
mailing list