[Agda] Instance arguments vs auto in Idris.

[Guillaume Brunerie]

Maybe there could be a way to declare an explicit argument to be
available for instance search (other than my hack above).
For instance

f : A -> B -> C
f (instance a) (instance b) = ?

Guillaume

On Tue, Oct 31, 2017 at 4:07 PM, Ulf Norell <ulf.norell at gmail.com> wrote:
> 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.html?#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
>>
>