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

Dominique Devriese dominique.devriese at cs.kuleuven.be
Fri Apr 1 15:27:40 CEST 2011


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


More information about the Agda mailing list