[Agda] stdlib for practical programming

[Sergei Meshveliani]

On Thu, 2013-09-26 at 18:29 +0300, Dmytro Starosud wrote:
> I didn't mean full support of "classes" in Agda.
> I wanted just some library, implemented in Agda using
> instance/implicit arguments, allowing functions overloading.
> Also I looked into
> http://www2.tcs.ifi.lmu.de/~abel/repos/AgdaPrelude/, which would be
> exactly what I need.
> But I see it hasn't been supported for a long time.
> Have you seen anything else?
> 
> Best regards,
> Dima


What do you mean for "some library" ?
For example, is Standard library  lib-0.7  "some library" ?

> Also I looked into
> http://www2.tcs.ifi.lmu.de/~abel/repos/AgdaPrelude/, which would be
> exactly what I need.
> But I see it hasn't been supported for a long time.
> Have you seen anything else?

There is some confusion here.
I follow this link, and read there, in READMWE.agda:

  module README where

  ------------------------------------------------------------------------
  -- The Agda standard library
  --
  -- Author: Nils Anders Danielsson, with contributions from Andreas
  -- []
  -- []


Probably, this is precisely the  Agda Standard library.
May be this is an old version.
But you can download a fresh version of  lib-0.7  from 

    http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary

It is supported. This library has many useful things, and is very good. 
And it does allow/use function overloading

(what people tell: does it?).

I think, the Agda language itself supports overloading

(what people tell: does it?),

and Standard library exploits this, as well as most user programs. 

What do you mean by function overloading?
For example, I thought that my below examples with  natPair+group  and  lDecSetoid
present overloading for the operations _+_ and _≟_.
Do they?

Regards,

------
Sergei
 

> 2013/9/26 Sergei Meshveliani <mechvel at botik.ru>:
> > 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.
> >
>