[Agda] stdlib for practical programming

[Sergei Meshveliani]

On Wed, 2013-09-25 at 19:36 +0300, Dmytro Starosud wrote:
> By "implicit parameters" do you mean {{instance}} parameters?
> 
> Thanks,
> Dima
> 
> 2013/9/24 Sergei Meshveliani <mechvel at botik.ru>:
> > On Tue, 2013-09-24 at 19:00 +0300, Dmytro Starosud wrote:
> >> Hello everybody!
> >>
> >> I would like to use Agda for practical programming rather just proof checker.
> >> For this purpose I need library with type classes and stuff for IO
> >> operations which would make easier fast prototyping.
> >> [..]
> >
> > After 1 year experience with writing a computer algebra library in Agda
> > I start to think that classes are not needed, that
> > dependent records + implicit parameters  of Agda is better.



Please, withdraw my previous respond. Here is the improved one.  

--------------------------------------------
Yes,  {{instance}}  parameters also.
For example:

  nat+group     = ...  -- : Group       
  natPair+group = ...  -- : Group                            

  f : ℕ → ℕ × ℕ → ℕ
  f m (n1 , n2) =  m + sum2 ((n1 , n2) + (0, 1)) 
                   where
  	       	   sum2 (k , l) = k + l
                   open Group {{...}}

Here  nat+group  is the instance of the additive Group for   ℕ,
_+_           is the operation of such a group,
natPairGroup  is the instance of the additive Group for   ℕ × ℕ
(suppose that these two instances are built earlier),

the implementation of  f  uses _+_ as both of ℕ and of ℕ × ℕ.

Here is a concrete example, which is type-checked:

------------------------------------------------------------------------
open import Function using (case_of_)
open import Relation.Binary using (DecSetoid; module DecSetoid;
                                   DecTotalOrder; module DecTotalOrder)
open import Relation.Nullary.Core using (yes; no)
open import Data.Nat as Nat       using (ℕ;  decTotalOrder)
open import Data.List             using (List; []; _∷_)
open import Relation.Binary.List.Pointwise as LP using (decSetoid)

f : ℕ → List ℕ → List ℕ
f _ []       =  []
f x (y ∷ ys) =  case x ≟ y of \
                     { (yes _) → case ys ≟ zs of \ { (yes _) → []
                                                   ; (no _)  → x ∷ ys }
                     ; (no _)  → ys
                     }
  where
  natDecSetoid = DecTotalOrder.Eq.decSetoid Nat.decTotalOrder
  lDecSetoid   = LP.decSetoid natDecSetoid
  open DecSetoid {{...}}

  zs = 0 ∷ 1 ∷ []
------------------------------------------------------------------------

It uses the same symbol  _≟_  to decide equality on  ℕ  and on  List ℕ
in the same scope in the `case' expression.

_≟_ is an operation of the `class' DecSetoid. 

The instance   natDecSetoid  of  DecSetoid  is extracted from the
library instance of DecTotalOrder for ℕ.  
The instance of   lDecSetoid  of DecSetoid  is for  List ℕ,
it is built by applying a library function  LP.decSetoid to
natDecSetoid.

I do not know of whether  open Foo {{...}}  will serve so nicely in a
more complex environment, but at least this sets a question:

  why do we need classes, if this example done by implicit instance
  arguments?

Can people provide a simple example showing that classes are desirable?

Another point on classes it that classes will be (if implemented) given
not in full but somewhat in 2/3. This is due to the
language/implementation problem of _overlapping instances_.
For example, in advanced algebra, overlapping instances do appear.

Regards,

------
Sergei