[Agda] Newbie Questions

[Shin-Cheng Mu]

Hi,

I became interested in dependent type a while ago and have been
looking for a good language to practice with. Agda seems to be
a perfect candidate so far, so I have joined this mailing list
hoping to learn more. Pardon me if I start to ask lots of newbie
questions. :)

I.

I encountered some peculiar phenomena when using implicit
parameters. Define the usual datatype for lists indexed by
lengths as below:

   data List (a : Set) : Nat -> Set where
     [] : List a zero
     _::_ : {n : Nat} -> a -> List a n -> List a (suc n)

The function revcat, defined below, reverts its first argument
using the second argument as an accumulating parameter:

   revcat : {a : Set} -> {m n : Nat} ->
               List a m -> List a n -> List a (m + n)
   revcat [] ys = ys
   revcat {a} {suc m} {n} (x :: xs) ys =
          psuc {m} {n} {List a} (revcat xs (x :: ys))

Here psuc is a function type-casting all values of type
f (m + suc n) to type f (suc m + n), for arbitrary f
(definition given below. I did not know that I could have
used +suc in Data.Nat.Properties instead).

The revcat above works fine. If I omit the implicit parameters,

   revcat (x :: xs) ys = psuc (revcat xs (x :: ys))

I would expect the computer to tell me that it needs
more information to check the types.

Strangely, revcat defined without the implicit parameters
still typechecks. When I try to execute
revcat (1 :: (3 :: [])) (2 :: (4 :: [])) in the interpreter,
I get

    _86 1 1 (3 :: []) (2 :: (4 :: [])),

which seems to be an unevaluated expression. Does it not
violate the slogan that “well-typed programs don’t go wrong?”

II.

Another question. I tried to repeat the example in Altenkirch,
McBride, and McKinna’s "Why Dependent Type Matters". The following
datatype Tree intends to define a balanced tree:

   data Tree (a : Set) : Nat -> Set where
     Nul : Tree a zero
     Tip : a -> Tree a (suc zero)
     Bin : {m n : Nat} -> (p : Parity) ->
           Tree a (parity p + n) -> Tree a n -> Tree a (parity p + (n  
+ n))

where parity : Parity -> Nat.

Now, how do I match the size of a tree built with Bin? The following
did not work:

   insert : {a : Set} -> {n : Nat} ->
               a -> Tree a n -> Tree a (suc n)
   insert {a} {n} x (Bin Odd t u) = ...

The computer complains that "parity p + (n' + n') != n of type Nat."
Changing n to, for example p + (n + n), did not help..

Thanks!

sincerely,
Shin

Appendix. Definition of psuc and some misc. functions.

   psuc : {m : Nat} -> {n : Nat} -> {f : Nat -> Set} ->
               f (m + suc n) -> f (suc m + n)
   psuc {zero} {n} {f} xs = xs
   psuc {suc m} {n} {f} xs = psuc {m} {n} {f'} xs
      where f' : Nat -> Set
            f' n = f (suc n)

   data Parity : Set where
     Even : Parity
     Odd : Parity

   parity : Parity -> Nat
   parity Even = 0
   parity Odd = 1