[Agda] Recursive instance search limited in depth

[Edward Kmett]

I just want to mention as a data point the lack of recursive instance search is one of the things that prevents me from actively writing more Agda code today. Almost nothing I want to say is first-order enough that it can infer any arguments I actually want to use, and libraries like lens can't usefully be ported to Agda without it.

I would love to have a more principled story though, so I understand the current motivations, they just keep me stuck waiting in the wings. ;)

-Edward

On Oct 2, 2013, at 10:18 AM, Dominique Devriese <dominique.devriese at cs.kuleuven.be> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda