[Agda] Instance arguments vs auto in Idris.

[Ulf Norell]

There are a few reasons why only instance arguments are available for
instance search:

- Variables may have big types that are expensive to check against the goal
type. And you
  typically have quite a lot of variables in the context.

- Unrelated variables can interfere with instance search if their types
contain metas,
  meaning that instance search cannot determine uniqueness. In some cases
(don't
  have one at hand though), the metas in the types can only be solved once
the instance
  goal is solved, so you get an unsolved metas.

- It's a nice symmetric design: top-level things need to be 'instance' to
be eligible and
  lambda-bound things need to be '{{ }}'.

/ Ulf

On Tue, Oct 31, 2017 at 7:11 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> I haven't used Idris for a while but in the documentation, it says that
> using something in the outer context requires the "%hint" annotation, so
> this is similar to how we need to annotate functions with instance in Agda.
>
>  I am mostly referring to the lhs variables.
>
> What you propose is a nice hack that is only useful if the constructed
> proof is proportionally bigger.
>
> On Tue, Oct 31, 2017 at 8:01 PM, Guillaume Brunerie <
> guillaume.brunerie at gmail.com> wrote:
>
>> By "in the context", you only mean things bound by let and on
>> left-hand sides, right? Not everything in scope? Allowing everything
>> in scope would make instance search prohibitively slow when using big
>> libraries.
>>
>> If you do mean variables bound on left-hand sides, I’m not quite sure
>> either why explicit arguments are not available for instance search
>> but note that
>> - instance arguments *are* available for instance search, as you
>> mention, so even though in
>>
>> f : A -> B
>> f a = ?
>>
>> the [a] is not available for instance search in the goal, it is available
>> in
>>
>> f : {{_ : A}} -> B
>> f = ?
>>
>> - In case you need explicit arguments to be available for instance
>> search, you can use the following workaround:
>>
>> f : A -> B -> C
>> f a b = ? where instance _ = a; _ = b
>>
>> Now both [a] and [b] are available for instance search.
>>
>> On Tue, Oct 31, 2017 at 12:47 PM, Apostolis Xekoukoulotakis
>> <apostolis.xekoukoulotakis at gmail.com> wrote:
>> > http://docs.idris-lang.org/en/latest/tutorial/miscellany.htm
>> l?#auto-implicit-arguments
>> >
>> > On Tue, Oct 31, 2017 at 6:17 PM, Apostolis Xekoukoulotakis
>> > <apostolis.xekoukoulotakis at gmail.com> wrote:
>> >>
>> >> I am trying to simplify my code by using instance arguments and thus
>> >> letting agda fill them.
>> >>
>> >> I am wondering why Agda does not allow to pick variables that are not
>> >> instance tagged as solutions if there is a unique such solution in the
>> >> context.
>> >>
>> >> A similar feature is the 'auto' in Idris. In this case, auto specifies
>> >> which implicit arguments to automatically fill , with anything found
>> in the
>> >> context.
>> >
>> >
>> >
>> > _______________________________________________
>> > 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171031/5caf49fb/attachment-0001.html>