[Agda] Recursive instance search limited in depth

Guillaume Brunerie guillaume.brunerie at gmail.com
Wed Oct 2 15:41:48 CEST 2013


Hello,

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).
Is that the case or is it just that recursive instance search is more
complicated to implement?

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.

What do you think?
Is there something I’m missing or would it be accepted in Agda?

Thanks,

Guillaume


More information about the Agda mailing list