[Agda] Recursive instance search limited in depth
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Nov 4 18:04:23 CET 2013
Concerning recursive instance search, I have put up a (mostly
conservative) proposal at
http://code.google.com/p/agda/issues/detail?can=2&q=938
This would be not too hard to implement. It would also address
efficiency issues of the current implementation. Another problem that I
have with the current proposal would also vanish, namely that instance
resolution will happily use
postulate undefined : forall {a}{A : Set a} -> A
for everything (that has no other instance).
PROPOSAL:
Currently instance search considers every name that in scope as a
candidate. That would make recursive instance resolution forbiddingly
slow. Here is a proposal how to change the instance mechanism to
facilitate recursive instance resolution. I think it has been
discussed before. Maybe it is time for action.
1. Add an 'instance' keyword in the style of 'private' and 'abstract'
that classifies definitions as to be taken into account during
instance resolution. Example:
{-# OPTIONS --copatterns #-}
record RawMonoid {a} (A : Set a) : Set a where
field
nil : A
_++_ : A -> A -> A
open RawMonoid
instance
rawMonoidList : forall {a}{A : Set a} -> RawMonoid (List A)
rawMonoidList = record { nil = []; _++_ = List._++_ }
-- using copatterns to define this recursive instance:
rawMonoidMaybe : {A : Set}{{ m : RawMonoid A }} -> RawMonoid (Maybe A)
nil (rawMonoidMaybe {{m = m}}) = nothing
_++_ (rawMonoidMaybe {{m = m}}) nothing mb = mb
_++_ (rawMonoidMaybe {{m = m}}) ma nothing = ma
_++_ (rawMonoidMaybe {{m = m}}) (just a) (just b) = just (_++_ m a b)
Each definition is thus tagged as 'instance' or 'not instance'.
2. When searching for an instance, take all local bindings into
account plus the global 'instance' bindings. Also, search recursively.
For instance, searching for
? : RawMonoid (Maybe (List A))
will consider the candidates {rawMonoidList, rawMonoidMaybe}, fail to
unify the first one, succeeding with the second one
? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))
and continue with goal
?m : RawMonoid (List A)
This will then find
?m = rawMonoidList {a = lzero}{A = A}
and putting together we have the solution.
Uniqueness of instances should be up to definitional equality
(see Issue 899).
3. Restrictions on the type of instances:
a) Each type of an instance must end in (something that reduces to)
a record or data type.
This allows to build a simple index structure
data/record name --> possible instances
that speeds up instance search.
b) [Termination check] recursive instances must be at structurally
smaller types. This is the usual Haskell restriction.
Something better might be
How to exactly devise this termination check is not yet clear.
rawMonoidMaybe is obviously ok, since in the recursive call
RawMonoid A, A is smaller than (Maybe A).
4. Name space management.
No special management for now. If a definition is in scope, and it is
an instance, it will be used during instance search.
If you want a name x from module M but not as an instance, you can do
open module _ using (x) where
open module M renaming (x to y)
x = y
Maybe some import directive like
using instances
that only imports the instances would be convenient, time will tell.
Cheers,
Andreas
On 02.10.2013 22:54, Dominique Devriese wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list