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

[Andreas Abel]

Excellent!

Thanks for addressing issue!  Your solution is quite similar to Agda 1 
type classes.  Nothing has been moving on this front, so I am very glad 
someone picked up this issue.

Are you coming to the Agda meeting (starting next Wednesday)?  Then you 
could present you proposal and discuss it with the developers.

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=AIMXIII.ProgramEtc

In your paper you are addressing the question of a logic programming 
engine to find instances and proofs.  Indeed, I think such an engine 
would be useful if it sensibly restricted (no recursion) and also only 
succeeds if there is a *unique* instance.  In case of proofs (see the 
irrelevance feature) uniqueness is not important, but surely in case of 
inferred programs (as it is with unification now).

Cheers,
Andreas

On 4/1/11 3:27 PM, Dominique Devriese 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
>