[Agda] Recursive instance search
Ulf Norell
ulf.norell at gmail.com
Mon Jul 14 09:49:22 CEST 2014
Merged.
/ Ulf
On Sun, Jul 13, 2014 at 4:47 PM, Ulf Norell <ulf.norell at gmail.com> wrote:
> 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/20140714/46c4fe7d/attachment-0001.html
More information about the Agda
mailing list