[Agda] Instance arguments vs auto in Idris.

[Ulf Norell]

You can also define a function

infixr 0 _asInst_
  _asInst_ : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → ({{y : A}} → B
y) → B x
  x asInst f = f {{x}}

and say

f : A -> B -> C
f a b = a asInst b asInst ?

I think pattern synonyms is the best vehicle to solve this problem.
Currently they
don't support instance arguments, but that's been on my todo list for a
while. I
filed #2829:

https://github.com/agda/agda/issues/2829

/ Ulf

On Tue, Oct 31, 2017 at 9:10 PM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> 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
> >>
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171101/55a3731b/attachment.html>