[Agda] Agda for CA

[Serge D. Mechveliani]

People, 
I investigate the possibility to write  computer algebra  using a 
language with dependent types which parameter values may be evaluated
at run time.
And it is desirable for this language to be possibly close to Haskell.
I have looked into the Agda tutorial, and have the following beginner 
questions.

1. Is Agda evaluation lazy? 

2. Is Adga going to join (multiparametric) type classes?
2.1. They say that type classes can be easily modelled in Adga by 
     dependent records, or/and may be, by implicit arguments.
Is this so?
If yes, how would it look the Agda program corresponding to the 
Haskell program

---------------------------------------------------------------------
class Eq a where (==) :: a -> a -> Bool
instance Eq Bool where  True  == True = true
                        True  == _    = false
                        False == True = false
                        False == _    = true 

instance Eq a => Eq [a] where  []      == [] = true
                               []      == _  = false
                               (_: _)  == [] = false
                               (x: xs) == (y: ys) ==  x == y && xs == ys 
f :: [Bool] -> Bool 
f xs =  xs == [True, False, True]
---------------------------------------------------------------------

(a contrived example, not tried to compile)
?

3. Here are the two examples of dependent type usage in computer algebra.

3.1.
The domain  Matrix R n m   is represented by a list of  n  rows,
each row being a list of  m  elements of a  type R,   n, m > 0.

For  R  belonging to the class  CommutativeRing,
  Matrix R n m   must have the instance of  MultipicativeSemigroup 
  (by `*')  iff  n == m.

And  m, n  are often computed at run time.

3.2. The domain  D = RtPolynomial vars,  length vars > 0. 
  is polynomials with Rational coefficients in the variable list  vars.
In many methods, the list  vars  is computed at run time.
Depending on  (length vars),  different instance set needs to be defined 
for  D.  For example,  D is Euclidean  iff  (length vars) == 1.

Please, copy the response to  mechvel at botik.ru

Thanks,

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