[Agda] stdlib for practical programming
Paolo Capriotti
p.capriotti at gmail.com
Thu Sep 26 11:55:07 CEST 2013
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
More information about the Agda
mailing list