[Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]

[Frédéric Blanqui]

Le 25/08/2020 à 12:49, András Kovács a écrit :
> Frédéric: by solving only pattern unification problems, which have 
> definitionaly unique solutions,

Could you provide a reference please?


> and reducing every non-pattern problem to pattern problems by various 
> strategies, e.g. by constraint postponing or eta conversion.
>
> However, this uniqueness is only about unification, but that's just 
> one part of elaboration. There is also a degree of freedom in deciding 
> where to insert implicit applications and lambdas, and Agda's choice 
> of insertions is not really unique. In general, I think it's 
> practically realistic to have unification which produces unique 
> solutions, but not that realistic to have elaboration which produces 
> unique output.
>
> Frédéric Blanqui <frederic.blanqui at inria.fr 
> <mailto:frederic.blanqui at inria.fr>> ezt írta (időpont: 2020. aug. 25., 
> K, 12:33):
>
>     Hi. How do you know that a unification problem in Agda (hence modulo
>     definitional equality right?) has a unique solution?
>
>     Le 25/08/2020 à 10:56, Nils Anders Danielsson a écrit :
>     > On 2020-08-25 06:42, Henning Basold wrote:
>     >> reasoning about commuting diagrams in category theory is quite
>     neat to
>     >> do in Agda, although better heuristics to figure out implicit
>     >> arguments need to be implemented.
>     >
>     > Unlike several other systems Agda does not instantiate implicit
>     > arguments unless the solution is unique (if we ignore bugs). Do
>     you have
>     > an example where Agda fails to find a unique solution, and you think
>     > Agda should have found it? In that case, please post it on the bug
>     > tracker.
>     >
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto: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/20200825/2f9a2e7e/attachment.html>