[Agda] stdlib for practical programming

[Dmytro Starosud]

OK, I see I should have been more precise.
Yes, Standard library is "some library" but it doesn't allow enough
level of overloading.
What I need? A lot of stuff.
In particular I need map (fmap, _<$>_ whatever) function which will
work for any functor (Maybe, List, Vector, Product, mapable; IMapable
whatever).
I don't want import renaming ten modules just to do some simple things.
I was asking for library, which simplifies all this work.
e.g. I would like following:

open import Prelude -- Prelude is this wanted "some library"
{- many useful stuff here -}

instead of:

open import Level renaming (zero to zeroL; suc to sucL; \lub to \lubL)
open import Data.Nat renaming (zero to zeroN; suc to sucN; \lub to \lubN; ...)
open import Data.List renaming (map to mapL; foldr to foldrL; ...)
open import Data.Vector renaming (map to mapV; foldr to foldrV; ...)
open import Data.Product renaming (map to mapP; ...)
etc. ...
etc. ...
etc. ...

{- many useful stuff here -}

Best regards,
Dmytro

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