[Agda] Instance arguments vs auto in Idris.

http://docs.idris-lang.org/en/latest/tutorial/miscellany.html?#auto-implicit-arguments

On Tue, Oct 31, 2017 at 6:17 PM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
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.

Guillaume Brunerie

2017-10-31 18:01:10 UTC

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

Post by Apostolis Xekoukoulotakis
http://docs.idris-lang.org/en/latest/tutorial/miscellany.html?#auto-implicit-arguments
On Tue, Oct 31, 2017 at 6:17 PM, Apostolis Xekoukoulotakis

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Apostolis Xekoukoulotakis

2017-10-31 18:11:15 UTC

This post might be inappropriate. Click to display it.

Ulf Norell

2017-10-31 20:07:12 UTC

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 <

Post by Apostolis Xekoukoulotakis
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 <

Post by Guillaume Brunerie
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
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

Post by Apostolis Xekoukoulotakis
http://docs.idris-lang.org/en/latest/tutorial/miscellany.htm

l?#auto-implicit-arguments

Post by Apostolis Xekoukoulotakis
On Tue, Oct 31, 2017 at 6:17 PM, Apostolis Xekoukoulotakis

in the

Post by Apostolis Xekoukoulotakis
context.

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Guillaume Brunerie

2017-10-31 20:10:33 UTC

This post might be inappropriate. Click to display it.

Ulf Norell

2017-11-01 09:22:48 UTC

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 <

Post by 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

Post by Ulf Norell
There are a few reasons why only instance arguments are available for
- Variables may have big types that are expensive to check against the

goal

Post by Ulf Norell
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

Post by Ulf Norell
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

Post by Ulf Norell
eligible and
lambda-bound things need to be '{{ }}'.
/ Ulf
On Tue, Oct 31, 2017 at 7:11 PM, Apostolis Xekoukoulotakis

Agda.

Post by Apostolis Xekoukoulotakis
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

available

Post by Guillaume Brunerie
in
f : {{_ : A}} -> B
f = ?
- In case you need explicit arguments to be available for instance
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

Post by Apostolis Xekoukoulotakis
http://docs.idris-lang.org/en/latest/tutorial/miscellany.

html?#auto-implicit-arguments

Post by Apostolis Xekoukoulotakis
On Tue, Oct 31, 2017 at 6:17 PM, Apostolis Xekoukoulotakis

Post by Apostolis Xekoukoulotakis
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

Post by Apostolis Xekoukoulotakis
instance tagged as solutions if there is a unique such solution in

the

Post by Apostolis Xekoukoulotakis
context.
A similar feature is the 'auto' in Idris. In this case, auto

specifies