[Agda] beginner questions

[Andreas Abel]

The questions on the standard library are best answered by Nisse...

On 23.07.2012 14:04, Serge D. Mechveliani wrote:
> 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 :: [])

eq is an "overloaded" function in the sense that it expects an instance 
argument {{ ... }}.  The instance argument is found by Agda 
automatically if something of the correct type is in scope, in this 
case, listBoolEq.

Dot notation does not work for records in Agda.


Being explicit about hidden arguments, you could write

    eq {{ listEq eqBool }} (true :: ...



> (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' ?

a : Level is a universe level.  If you omit it, it defaults to 0.  So

   T : Set

just means

   T : Set Level.zero

or

   T : Set0

which is sometimes voices as "T is a small type".  T : Set1 would be "T 
is a big type", but  T : Set2 would be an even bigger type...

> (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  ()  -- ?

Since 19 < 26 computes to true, isTrue (19 < 26) computes to the unit 
type which is the Agda representation of the proposition "True".  So, to 
prove isTrue (19 < 26) you only need an inhabitant of the unit type.  An 
underscore _ suffices.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/