[Agda] Instance arguments and types who have a unique construction.

[Apostolis Xekoukoulotakis]

Currently, instance resolution tries all possible ways to construct an
instance argument.

It will look for arguments in the environment and it will use instance
functions to create new ones. If there are multiple solutions, instance
resolution will fail.

example :

Assuming we have defined "less than" as instance.

if we have in the context, a variable q with type zero ≀ (suc zero) ,
instance resolution will fail because there are two solutions, q and z≀n.

But q is in fact z≀n.


We can prove that there is only one possible construction of the type, thus
any variables with the same type are the same.

At the moment, I am trying to prune my context but it would be nice if
instance resolution was a bit smarter.

[Ulf Norell]

Instance search does check solutions for *definitional* equality. The
problem in your case is that `q` is only propositionally (provably) equal
to `z≀n`. I think it's a bit too much to ask of instance search that it
would look for proofs that two candidate solutions are equal.

Did you have a particular suggestion for what kind of smartness improvement
would make this work?

/ Ulf

On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
Currently, instance resolution tries all possible ways to construct an
instance argument.
It will look for arguments in the environment and it will use instance
functions to create new ones. If there are multiple solutions, instance
resolution will fail.
Assuming we have defined "less than" as instance.
if we have in the context, a variable q with type zero ≀ (suc zero) ,
instance resolution will fail because there are two solutions, q and z≀n.
But q is in fact z≀n.
We can prove that there is only one possible construction of the type,
thus any variables with the same type are the same.
At the moment, I am trying to prune my context but it would be nice if
instance resolution was a bit smarter.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Apostolis Xekoukoulotakis]

I do not know.

From a use case point of view, I would like to provide a proof that all
construction of a type are equal.

"∀ x y → (a : x ≀ y) → (b : x ≀ y) → a ≡ b" , and then use this proof to
merge all solutions into one.

Is this possible today ?

Post by Ulf Norell
Instance search does check solutions for *definitional* equality. The
problem in your case is that `q` is only propositionally (provably) equal
to `z≀n`. I think it's a bit too much to ask of instance search that it
would look for proofs that two candidate solutions are equal.
Did you have a particular suggestion for what kind of smartness
improvement would make this work?
/ Ulf
On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
Currently, instance resolution tries all possible ways to construct an
instance argument.
It will look for arguments in the environment and it will use instance
functions to create new ones. If there are multiple solutions, instance
resolution will fail.
Assuming we have defined "less than" as instance.
if we have in the context, a variable q with type zero ≀ (suc zero) ,
instance resolution will fail because there are two solutions, q and z≀n.
But q is in fact z≀n.
We can prove that there is only one possible construction of the type,
thus any variables with the same type are the same.
At the moment, I am trying to prune my context but it would be nice if
instance resolution was a bit smarter.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Ulf Norell]

The more fundamental problem here is that it does actually matter which
solution we
pick when they aren't definitionally equal, even in the case when they are
provable equal.
It might well be the case that picking `q` is the right choice and picking
`z≀s` is wrong and
doing so would result in a type error further down in the code.

/ Ulf

On Thu, Jan 11, 2018 at 10:28 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
I do not know.
From a use case point of view, I would like to provide a proof that all
construction of a type are equal.
"∀ x y → (a : x ≀ y) → (b : x ≀ y) → a ≡ b" , and then use this proof to
merge all solutions into one.
Is this possible today ?

Post by Ulf Norell
Instance search does check solutions for *definitional* equality. The
problem in your case is that `q` is only propositionally (provably) equal
to `z≀n`. I think it's a bit too much to ask of instance search that it
would look for proofs that two candidate solutions are equal.
Did you have a particular suggestion for what kind of smartness
improvement would make this work?
/ Ulf
On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
Currently, instance resolution tries all possible ways to construct an
instance argument.
It will look for arguments in the environment and it will use instance
functions to create new ones. If there are multiple solutions, instance
resolution will fail.
Assuming we have defined "less than" as instance.
if we have in the context, a variable q with type zero ≀ (suc zero) ,
instance resolution will fail because there are two solutions, q and z≀n.
But q is in fact z≀n.
We can prove that there is only one possible construction of the type,
thus any variables with the same type are the same.
At the moment, I am trying to prune my context but it would be nice if
instance resolution was a bit smarter.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Apostolis Xekoukoulotakis]

I think I understand what you mean.

Let me see if I can prune my context then.

Post by Ulf Norell
The more fundamental problem here is that it does actually matter which
solution we
pick when they aren't definitionally equal, even in the case when they are
provable equal.
It might well be the case that picking `q` is the right choice and picking
`z≀s` is wrong and
doing so would result in a type error further down in the code.
/ Ulf
On Thu, Jan 11, 2018 at 10:28 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
I do not know.
From a use case point of view, I would like to provide a proof that all
construction of a type are equal.
"∀ x y → (a : x ≀ y) → (b : x ≀ y) → a ≡ b" , and then use this proof to
merge all solutions into one.
Is this possible today ?

Post by Ulf Norell
Instance search does check solutions for *definitional* equality. The
problem in your case is that `q` is only propositionally (provably) equal
to `z≀n`. I think it's a bit too much to ask of instance search that it
would look for proofs that two candidate solutions are equal.
Did you have a particular suggestion for what kind of smartness
improvement would make this work?
/ Ulf
On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
Currently, instance resolution tries all possible ways to construct an
instance argument.
It will look for arguments in the environment and it will use instance
functions to create new ones. If there are multiple solutions, instance
resolution will fail.
Assuming we have defined "less than" as instance.
if we have in the context, a variable q with type zero ≀ (suc zero) ,
instance resolution will fail because there are two solutions, q and z≀n.
But q is in fact z≀n.
We can prove that there is only one possible construction of the type,
thus any variables with the same type are the same.
At the moment, I am trying to prune my context but it would be nice if
instance resolution was a bit smarter.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Guillaume Brunerie]

Have you tried to use irrelevance?
As far as I understand, it does basically what you want, by somehow making
all elements of the type x ≀ y definitionally equal to each other.
I haven’t tried, so I don’t know if it interacts well with instance
arguments.

Guillaume

On Thu, Jan 11, 2018 at 11:00 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
I think I understand what you mean.
Let me see if I can prune my context then.

Post by Ulf Norell
The more fundamental problem here is that it does actually matter which
solution we
pick when they aren't definitionally equal, even in the case when they
are provable equal.
It might well be the case that picking `q` is the right choice and
picking `z≀s` is wrong and
doing so would result in a type error further down in the code.
/ Ulf
On Thu, Jan 11, 2018 at 10:28 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
I do not know.
From a use case point of view, I would like to provide a proof that all
construction of a type are equal.
"∀ x y → (a : x ≀ y) → (b : x ≀ y) → a ≡ b" , and then use this proof to
merge all solutions into one.
Is this possible today ?

Post by Ulf Norell
Instance search does check solutions for *definitional* equality. The
problem in your case is that `q` is only propositionally (provably) equal
to `z≀n`. I think it's a bit too much to ask of instance search that it
would look for proofs that two candidate solutions are equal.
Did you have a particular suggestion for what kind of smartness
improvement would make this work?
/ Ulf
On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
Currently, instance resolution tries all possible ways to construct an
instance argument.
It will look for arguments in the environment and it will use instance
functions to create new ones. If there are multiple solutions, instance
resolution will fail.
Assuming we have defined "less than" as instance.
if we have in the context, a variable q with type zero ≀ (suc zero) ,
instance resolution will fail because there are two solutions, q and z≀n.
But q is in fact z≀n.
We can prove that there is only one possible construction of the type,
thus any variables with the same type are the same.
At the moment, I am trying to prune my context but it would be nice if
instance resolution was a bit smarter.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

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

[Apostolis Xekoukoulotakis]

I tried it before.
If I am desperate, I might use it again :).

On Thu, Jan 11, 2018 at 2:55 PM, Guillaume Brunerie <

Post by Guillaume Brunerie
Have you tried to use irrelevance?
As far as I understand, it does basically what you want, by somehow making
all elements of the type x ≀ y definitionally equal to each other.
I haven’t tried, so I don’t know if it interacts well with instance
arguments.
Guillaume
On Thu, Jan 11, 2018 at 11:00 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
I think I understand what you mean.
Let me see if I can prune my context then.

Post by Ulf Norell
The more fundamental problem here is that it does actually matter which
solution we
pick when they aren't definitionally equal, even in the case when they
are provable equal.
It might well be the case that picking `q` is the right choice and
picking `z≀s` is wrong and
doing so would result in a type error further down in the code.
/ Ulf
On Thu, Jan 11, 2018 at 10:28 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
I do not know.
From a use case point of view, I would like to provide a proof that all
construction of a type are equal.
"∀ x y → (a : x ≀ y) → (b : x ≀ y) → a ≡ b" , and then use this proof
to merge all solutions into one.
Is this possible today ?

Post by Ulf Norell
Instance search does check solutions for *definitional* equality. The
problem in your case is that `q` is only propositionally (provably) equal
to `z≀n`. I think it's a bit too much to ask of instance search that it
would look for proofs that two candidate solutions are equal.
Did you have a particular suggestion for what kind of smartness
improvement would make this work?
/ Ulf
On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
Currently, instance resolution tries all possible ways to construct
an instance argument.
It will look for arguments in the environment and it will use
instance functions to create new ones. If there are multiple solutions,
instance resolution will fail.
Assuming we have defined "less than" as instance.
if we have in the context, a variable q with type zero ≀ (suc zero) ,
instance resolution will fail because there are two solutions, q and z≀n.
But q is in fact z≀n.
We can prove that there is only one possible construction of the
type, thus any variables with the same type are the same.
At the moment, I am trying to prune my context but it would be nice
if instance resolution was a bit smarter.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

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