[Agda] Agda for CA

[Andreas Abel]

On 15.07.2012 19:58, Serge D. Mechveliani wrote:
> 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?

Yes.

Although, I'd say, a bit too lazy at the moment.  Internally, Agda is 
doing call-by-name.  Agda code compiled to Haskell of course uses 
call-by-need.

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

Yes.

Currently, however there is no recursive instance search.  E.g. in your 
example, you will have to locally instantiate list equality to Bool. 
See below for an example.

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

I am copying code from examples/instance-arguments/06-listEquality.agda
It does roughly what you want:

module 06-listEquality where

infixr 5 _∷_

data List (A : Set) : Set where
   []  : List A
   _∷_ : (x : A) (xs : List A) → List A

data Bool : Set where
   true : Bool
   false : Bool

id : {A : Set} → A → A
id v = v

or : Bool → Bool → Bool
or true _ = true
or _ true = true
or false false = false

and : Bool → Bool → Bool
and false _ = false
and _ false = false
and true true = false

not : Bool → Bool
not true = false
not false = true

record Eq (A : Set) : Set where
   field eq : A → A → Bool

listEq : {A : Set} → Eq A → Eq (List A)
listEq {A} eqA = record { eq = eq' } where
   eq' : List A → List A → Bool
   eq' [] [] = true
   eq' (a ∷ as) (b ∷ bs) = and (Eq.eq eqA a b) (eq' as bs)
   eq' _ _ = false

primEqBool : Bool → Bool → Bool
primEqBool true = id
primEqBool false = not

eqBool : Eq Bool
eqBool = record { eq = primEqBool }

open Eq {{...}}

test = eq (true ∷ false ∷ true ∷ []) (true ∷ false ∷ [])
   where listBoolEq = listEq eqBool



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

This can be represented in Agda.

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/