[Agda] Recursive instance search limited in depth

[Dominique Devriese]

Hi Guillaume,

2013/10/2 Guillaume Brunerie <guillaume.brunerie at gmail.com>:
> In Dominique Devriese and Frank Piessens’s paper "On the Bright Side
> of Type Classes:
> Instance Arguments in Agda" they say (section 4.1) that having
> recursive instance search is not desirable in Agda, because it would
> be powerful and Agda should not be too powerful :-) (or at least this
> is what I understood).

Actually the argument is that the *instance search* should not be too
powerful and we should find a way to use Agda's existing type-level
computation instead.  I like  the approach in Dmitry Starosud's previous
mail of trying to achieve results similar to parametric instances using
Agda's existing type-level computation, although it's not clear to me
how to avoid the no-termination-check requirement and whether it can't
be abused to prove false somehow.

> Is that the case or is it just that recursive instance search is more
> complicated to implement?

I do not think this would be very difficult to implement actually.  I think you
would want to add some way of marking values eligible for instance
resolution (because combining the current "all values are
automatically considered" with a recursive search seems like it would
require too much work from the typechecker).  You would obviously need
to add a way to declare parametric instances and implement the search,
but I see no major obstacles.

Should you implement this, you should be careful though because the
instance search introduced for instance arguments is currently also
used for other purposes (something related to irrelevant arguments,
but I should check the details).  I'm not sure what the best approach
there would be...

However, despite the technical ease of implementation, I still think
it's worth carefully considering if Haskell's (Prolog without
backtracking)-like instance search (or even worse the search for Coq's
canonical structures) is an example we want to follow in the long term...
On a related note: in a Haskell Symposium panel discussion last week,
Doaitse Swierstra argued against Haskell's instance resolution and its
various extensions as a part of the language that is complex and
hard to explain to beginners in the language. Nevertheless, I am aware
that there are practical examples not covered by the current instance
search and I can't offer a practical alternative for some use cases.

Maybe it would not be so bad to add parametric instances if we keep
the parametric instances' patterns linear and structurally recursive
to at least keep a functional model?  Non-linear parametric instances
could probably be easily abused to decide equality of types, which I
think we want to avoid.

> In any case, there is another option which seems quite easy to
> implement, not too powerful but probably still very useful: limit
> instance search to a given depth.
> There could be a flag similar to --termination-depth (maybe
> --instance-search-depth) where the user specifies a number n, and then
> Agda would limit instance search depth to n.

This is an interesting suggestion, but I would still prefer an
approach that is somehow based on Agda's existing, functional type-level
computational model, perhaps somehow based on the ideas in
Dmitry Starosud's previous mail?

Regards
Dominique