[Agda] standard instance proposal

[Serge D. Mechveliani]

People,

Here is a certain  Product & List instance  proposal for 
Standard Library.

(I)
  productSetoid : {c l c' l' : Level} -> (A : Setoid c  l ) -> 
                                         (B : Setoid c' l') -> Setoid _ _

builds the setoid  A x B  for setoids A and B  defined by the standard
law for direct product
(is such in the library?).

The precise code is attached to this letter.


(II) listSetoid  for  List   needs to be defined similarly 
     (Erdi Gergo has recently sent the code). 
     (is such in the library?).

(III)
  setoidByMap : {c c' l' : Level} -> (C : Set c) -> (B : Setoid c' l') ->
                                     (C -> Setoid.Carrier B) -> Setoid _ _

builds the setoid  A  on  C  from a setoid  B  and a map 
f : C -> Carrier B   -- in a natural way:
a =C a' =  f a \~~ f a'.    

(is such in the library?).

The precise code zip archive is attached to this letter.
The code for  productSetoid  is of  40 lines, with comments,  
         for  setoidByMap    --     10 lines.

(VI) A similar instance map can be applied for  Semigroup, Group, 
     and some other Standard Library instances
     (direct product of Groups,  
      Ring of  R x R x ... x R  build via the instance map for Vector,
      and such
     ).
     
About generic programming
-------------------------
This is the generic programming of which  Joachim Breitner wrote recently:
 
> to me it rather seems that there is a need for some generic programming,
> i.e. a solution that works for all algebraic data types, or at least for
> simple enough ones such as List or the simple data type Gen 
> [..]

I have the two questions.

1. The  Haskell  library has the constructor class  Functor  which allows 
to apply  fmap  (as `map') not only to List but uniformly, to  List, 
Maybe a,  to any type constructor of the class Functor.
Is this of this generic programming ?

2. Concerning  setoidByMap :
it spreads the Setoid instance from  x (Product)  and  List  to a great 
family of constructs (by any map, by surjection, by bijection).

Does this `by map' approach replace the generic programming mentioned by 
Joachim Breitner ?

Here is an example of usage.
I have 
  record UMonomial {c l : Level} {dS : DSet c l} (R : Prering c l {dS}) :
                                                                    Set _ 
       where
       private decS = DSet.decSetoid dS
               0#   = Prering.0# R
       open DecSetoid {{...}}
       field  coef    : Carrier
              exp     : Nat
              coef/=0 : \neg (coef \~~ 0#) 

-- a monomial consists of a non-zero coefficient  coef : R  and  
exponent  exp : Nat.

The following function uses  productSetoid  and  setoidByMap  to build 
the setoid for  UMonomial R: 

  uMon-setoid : {c l : Level} -> (R : Prering c l) -> Setoid _ _
  uMon-setoid R =  setoidByMap (UMonomial R) R-x-Nat-setoid toProduct
    where
    natSetoid = <extract  Setoid  for  Nat  from Standard Library>
    decS      = Prering.decSetoid R  
    open DecSetoid decS renaming (Carrier to R-Carrier; 
                                                     setoid to R-setoid)
    R-x-Nat-setoid = productSetoid R-setoid natSetoid 
    open UMonomial
    toProduct : UMonomial R -> R-Carrier x Nat 
    toProduct mon = (coef mon , exp mon)

I propose 
(1) To include  setoidByMap, productSetoid, listSetoid, vectorSetoid,
    to the Standard Library
    (the code for the first three is ready),

(2) to do the same for DecSetoid,

(3) to consider including to the Standard Library similar functions for 
    Ordering, Semigroup, Group ...

As to (3), I need to add the folowing comment.
I am trying to build the classical algebraic hierarhy of  Set, Semigroup, 
Group, ... SuchAndSuchRing, Field, LeftModuleOverRing, ...,  
and need to somewhat extend with certain additional attributes each of the 
Standard library `classes' of  Semigroup, Monoid, ..., CommutativeRing.
And so far, I fail to use the corresponding Standard classes as they are. 
So I try their modifications:  DSet, DSemigroup, DMonoid ...

Regards,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sugg.agda.zip
Type: application/zip
Size: 1042 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130110/aa4f3e14/sugg.agda.zip