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

[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 <
guillaume.brunerie at gmail.com> wrote:

> 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 <
> apostolis.xekoukoulotakis at gmail.com> wrote:
>
>> I think I understand what you mean.
>>
>> Let me see if I can prune my context then.
>>
>> On Thu, Jan 11, 2018 at 11:37 AM, Ulf Norell <ulf.norell at gmail.com>
>> wrote:
>>
>>> 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 <
>>> apostolis.xekoukoulotakis at gmail.com> wrote:
>>>
>>>> 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 ?
>>>>
>>>>
>>>> On Thu, Jan 11, 2018 at 11:20 AM, Ulf Norell <ulf.norell at gmail.com>
>>>> wrote:
>>>>
>>>>> 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 <
>>>>> apostolis.xekoukoulotakis at gmail.com> wrote:
>>>>>
>>>>>> 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.
>>>>>>
>>>>>> _______________________________________________
>>>>>> 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/20180113/2e56eced/attachment.html>