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

[Dominique Devriese]

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