[Agda] stdlib for practical programming

[Paolo Capriotti]

On Thu, Sep 26, 2013 at 12:49:39PM +0400, Sergei Meshveliani wrote:
> On Wed, 2013-09-25 at 19:36 +0300, Dmytro Starosud wrote:
> > By "implicit parameters" do you mean {{instance}} parameters?
> > 
> > Thanks,
> > Dima
> 
> Any arguments introduced as implicit.
> (So far I never used {{...}} !).
> 
> Also I use `open' + `renaming' helps. For example:
> 
>   let open Ring R  using (Carrier; _+_; _*_; +comm; *assoc) 
>       open Ring R' using () renaming (Carrier to C'; _+_ to _+'; 
>                                                      _*_ to _*'_) 
>   in
>   a b : Carrier ...
>   a + b  ... a * b  ...  +comm a b
> 
>   c d : C'
>   ... c +' d ... c *' d
> 
> Here  R and R'  are the two instances of Ring made earlier.
> 
> Well, with the Haskell instances,  c +' d  can probably be replaced with
> c + d,  because   a  and  c  come from different domains.
> 
> I wonder, can  Agda  arrange this?
> When two instances of Ring are in scope, how to use the same symbol 
> _+_ ?
> Say,  +  is used for Nat and for  Nat \times Nat  in the same scope,
> how to write the same symbol `+' ?

I have tackled this problem for my category theory library
(https://github.com/pcapriotti/agda-categories). My solution is not
entirely satisfactory, but it works, and it allows me to define
hierarchies of structures (think Semigroup > Monoid > Group > ...) and
deal with them easily.

You can read about it here:
http://paolocapriotti.com/agda-base/overloading.core.html

Here is a more introductory presentation:
http://cs.nott.ac.uk/~pvc/away-day-2013/inheritance-overloading.pdf

And slides: http://cs.nott.ac.uk/~pvc/away-day-2013/slides.pdf

Paolo