[Agda] Recursive instance search limited in depth

[Dominique Devriese]

Ack.  Note that I'm not trying to stand in the way of progress here
and I realise that a working but less principled solution could be
better than an absent principled one.

I also think the design of instance arguments can be modified to
support a recursive instance search, reusing the less controversial
elements of the design (syntax, implicit args-like instantiation, the
"open Eq {{...}}" stuff etc.).


In case anyone is interested in ideas for a more principled direction,
I can sketch some that I've been wanting to explore, but am a bit
stuck with.  The solution would be based on a form of implicit
arguments parametrised by the "tactic" used to solve them when they
are needed at a call-site.  For an equality type class, I imagine it
would look like this:

  equal : forall {t: Set} {{findEq | eqT : Eq t}} -> t -> t -> Bool

where findEq would be a previously defined tactic used to find values
of type |Eq t| when at call sites.  In a system based on the existing
quoteGoal machinery, findEq could look like:

  data UniverseX : Set where ...
  interpretUniverseX : UniverseX -> Set
  termToUniverseX : Term -> Maybe UniverseX
  eqForUniverseX : (code : UniverseX) -> Eq (interpretUniverseX code)

  whenJust : forall {a b} {A : Set a} -> (m : Maybe A) -> (A -> Set b) -> Set b
  whenJust (just x) F = F x
  whenJust nothing _ = Lift Top

  fromJust : forall {a b} {A : Set a} (F : A -> Set b) -> (m : Maybe
A) -> ((a : A) -> F a) -> whenJust m F
  fromJust F nothing _ = lift top
  fromJust F (just x) f = f x

  findEq : (t : Term) -> whenJust (termToUniverseX t) (Eq . interpretUniverseX)
  findEq t = fromJust (Eq . interpretUniverseX) (termToUniverseX t)
eqForUniverseX

Then "equal 2 3" would be treated like "equal {t = _t} {{eqT =
quoteGoal t in findEq t}} 2 3", inferred to "equal {t = Nat} {{eqT =
quoteGoal t in findEq t}} 2 3", which would evaluate to "equal {t =
Nat} {{eqT = findEq (def 'Eq [def 'Nat])}} 2 3", which findEq should
be able to solve.

Unfortunately, I am stuck on two problems.  First, I expect this
approach could be made to work for closed types t, but what is missing
is a way for findEq to declare that it needs other Eq instances from a
caller context.  For example, for an example like
  test : forall {t} -> Eq t -> List t -> List t -> Bool
  test eqT = equal
Then one would expect findEq to notice that it can use the existing Eq
t to construct the needed Eq (List t).  Unfortunately, quoteGoal
doesn't give access to the context. This problem is what triggered my
work on typed syntactic meta-programming presented at ICFP last week,
but that work is not ready for practical use (see paper).

Secondly, the above tactics would yield a form of *closed* type
classes, while one would like them to be open.  There would need to be
a way for findEq to take into account information added afterwards by
the user.  Again: the problem is that quoteGoal does not give access
to other definitions in the user's scope.

Perhaps there is a way to solve both problems by somehow combining
them with the existing open non-recursive instance arguments, but I
haven't figured that out yet. Or perhaps quoteGoal can be extended to
give access to the context and user's scope?

Regards
Dominique

2013/10/2 Edward Kmett <ekmett at gmail.com>:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda