[Agda] Recursive instance search

[Ulf Norell]

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/20140711/44da357a/attachment.html