[Agda] stdlib for practical programming

[Dmytro Starosud]

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

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.
>
> Regards,
>
> ------
> Sergei
>
>