[Agda] Recursive instance search

[Ulf Norell]

It's very nice! Also much faster than the previous implementation, I have
examples that uses a lot of instance arguments that run 5x faster now, not
to mention that you can leave out all the silly specialisations like Eq
(List Nat).

I had to do a bit of work to get constructor classes (like Monad and
Functor) to work:

I lifted the restriction on recursive instances when there are metas in the
goal. The reason for this is that you get instance constraints like Monad
_M, with a side constraint _M Nat == IO Nat. To avoid the looping behaviour
you described in the release notes I prevent instance search from
instantiating insufficiently constrained metas, but allow it to instantiate
_M in the example above.

Unless someone has found any big issues, I want to merge this into master.

/ Ulf


On Fri, Jul 11, 2014 at 7:32 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> Awesome work. For now, I put it in a branch 'classes' in the main repo and
> granted you commit rights. I will try it out on UlfNorell/agda-prelude,
> which uses a lot of instance arguments.
>
> / Ulf
>
>
> On Fri, Jul 11, 2014 at 12:26 PM, Guillaume Brunerie <
> guillaume.brunerie at gmail.com> wrote:
>
>> Hello all,
>>
>> As some of you know, I started working on recursive instance search
>> during the previous AIM and the code is now available on my GitHub
>> here : https://github.com/guillaumebrunerie/agda (should I open a pull
>> request against the official Agda?)
>>
>> The main outstanding issue is that there is no termination check yet
>> so if you’re not careful when defining your instances you can easily
>> make Agda loop.
>> Also, I haven’t really thought about namespace management, for
>> instance 'hiding' does not hide instances (but serialization should
>> work, though).
>>
>> I copy-pasted the relevant part of the CHANGELOG below (I borrowed
>> part of the text in issue 938) and you can also look at the two files
>> test/succeed/RecursiveInstanceSearch{,Level}.agda to see some more
>> advanced examples of recursive instance search.
>>
>> Of course I welcome any feedback/bug reports.
>>
>> Cheers,
>> Guillaume
>>
>>
>>
>>
>> * Instance search is now more efficient and recursive (see issue 938)
>>   (but without termination check yet)
>>
>>   A new keyword `instance' has been introduced (in the style of
>>   `abstract' and  `private') which must now be used for every
>>   definition/postulate that has to be taken into account during instance
>>   resolution. For example:
>>
>>     {-# OPTIONS --copatterns #-}
>>
>>     record RawMonoid (A : Set) : Set where
>>       field
>>         nil  : A
>>         _++_ : A -> A -> A
>>     open RawMonoid
>>
>>     instance
>>       rawMonoidList : {A : Set} -> 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 = nothing
>>       _++_ rawMonoidMaybe nothing mb = mb
>>       _++_ rawMonoidMaybe ma nothing = ma
>>       _++_ (rawMonoidMaybe {{m}}) (just a) (just b) = just (_++_ m a b)
>>
>>   Moreover, each type of an instance must end in (something that reduces
>>   to) a named type (e.g. a record, a datatype or a postulate). This
>>   allows us to build a simple index structure
>>
>>     data/record name  -->  possible instances
>>
>>   that speeds up instance search.
>>
>>   Instance search takes into account all local bindings and all global
>>   'instance' bindings and the search is recursive. 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 = A}
>>
>>   and putting together we have the solution.
>>
>>   Be careful that there is no termination check for now, you can easily
>>   make Agda loop by declaring the identity function as an instance. But
>>   it shouldn’t be possible to make Agda loop by only declaring
>>   structurally recursive instances (whatever that means).
>>
>>   Additionally:
>>
>>   * Uniqueness of instances is up to definitional equality (see issue 899)
>>
>>   * Instance search will not be attempted if there are unsolved metas in
>>     the goal. The issue is that trying to typecheck [? ++ ?] would
>>     generate a constraint of type `RawMonoid ?' to be solved by instance
>>     search, but unification with `rawMonoidMaybe' will succeed and
>>     generate a new constraint of type `RawMonoid ?2' to be solved by
>>     instance search, and so on, so Agda would loop.
>>
>>     As a special case, if none of the instances declared for that type
>>     is recursive, then instance search is attempted as usual even if
>>     there are unsolved metas (no risk of looping here).
>>
>>   * Instances of the following form are allowed:
>>
>>         Π-level : {n : ℕ} {A : Set} {B : A → Set}
>>                   {{_ : (a : A) → has-level n (B a)}}
>>                   → has-level n ((a : A) → B a)
>>
>>       When searching recursively for an instance of type `(a : A) →
>>       has-level n (B a)', a lambda will automatically be introduced and
>>       instance search will search for something of type `has-level n (B
>>       a)' in the context extended by `a : A'.
>>
>>   * There is no longer any attempt to solve irrelevant metas by instance
>>     search
>>
>>   * Constructors of records and datatypes are automatically added to the
>>     instance table
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140713/7ba0dd42/attachment.html