[Agda] Agda for CA

Serge D. Mechveliani mechvel at botik.ru
Sun Jul 15 19:58:58 CEST 2012

```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

---------------------------------------------------------------------
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

```