[Agda] Proposed Agda feature: non-canonical implicit arguments

[Jean-Philippe Bernardy]

You may want to glance at the list of criteria we developed to compare
Haskell type classes and C++ concepts. It may give you and indication
of what features were considered useful across widely different languages.

http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=124669

Cheers,
JP.

On Fri, Apr 1, 2011 at 3:27 PM, Dominique Devriese
<dominique.devriese at cs.kuleuven.be> wrote:
> All,
>
> I want to announce the availability of an extension of Agda with
> "non-canonical implicit arguments": a language feature intended as an
> alternative to Haskell type classes. My promotor Frank Piessens and I
> have submitted a paper about this proposal for consideration for the
> ICFP 2011 conference. I have made available a website containing some
> basic info, a link to the submitted draft for more details, and a link
> to a git repository with the implementation (as a branch of the latest
> Agda implementation):
>
>  http://people.cs.kuleuven.be/~dominique.devriese/agda-non-canonical-implicits/
>
> I hope some of you can find the time to take a look at the proposed
> feature, the draft submitted to ICFP and the implementation. I
> consider the implementation ready if not terribly documented. There
> are examples in examples/non-canonical-implicits in the repository. I
> hope the feature can be considered for inclusion in mainstream Agda.
> Frank and I welcome any feedback on the proposed feature, the
> submitted draft or the implementation, on or off this list as
> appropriate.
>
> Thanks in advance for your time,
> Dominique
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>