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

[Dominique Devriese]

Andreas,

2011/4/1 Andreas Abel <andreas.abel at ifi.lmu.de>:
> 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.

First of all, I know little about Agda 1, I have never actually used
or even seen it. What I know about Agda 1 Type Classes is limited and
only based on a presentation by Catarina Coquand I found online:

  http://types2004.lri.fr/SLIDES/coquand.pdf

This talk seems to be about a proposal for a feature that seems very
similar to Sozeau and Oury Coq type classes. I would definitely
appreciate it if someone could provide me with a better reference or
source of info about Agda 1 type classes. In our proposal, we make
some different design choices, which are explained in depth in the
draft linked to from the website in my previous mail.

> 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

I would like to come, but I heard about the AIM too late. It's
possible I can still make it there on Wednesday or Thursday, but I'm
not yet sure.

> 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).

If you're talking about the resolution algorithm for not explicitly
provided non-canonical implicit arguments, then indeed, we have
restricted this according to what you suggest. We have not taken into
account irrelevance, but it may be possible to extend our approach as
you suggest.

Dominique