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

[András Kovács]

> What is the elaborated right-hand side of f? Is it "id" or
"id {A = <something>}"?

Well, this is an example for something which may be up to taste, or which
may vary depending on the rest of the implementation. If "f" is a top-level
definition, and we use meta-freezing like in Agda, then "id {?A}" only
results in a useless frozen meta. If "f" is a local definition and we
expect "?A" to be solved, then it might make sense to insert the
application, or we might want to leave it polymorphic even in that case. We
might even have let-generalization, in which case we can insert application
but immediately re-generalize. Or we might have some mechanism for delaying
insertions.

> Can you elaborate on this?

To define what uniqueness of elaboration means, we have to specify a
relation between core syntax and surface syntax, which holds when a core
term is a valid elaboration of a surface term. A sensible definition for
this relation is that the core term can only contain filled holes and extra
implicit insertions relative to the surface syntax. I think that this is
not quite enough, because it allows insertion of arbitrary number of
superfluous implicit lambdas, e.g. we may elaborate "let x = true in x" to
"let x = \{x : Bool} -> true in x {true}". So I think we should also add a
condition like "inserted implicit lambdas must have actually dependent
implicit function types", so "\{x : Bool} -> true" is illegal because it
has type "{x : Bool} -> Bool". So there's already a bit of a complication
when we try to define what uniqueness of elaboration means.

Anyway, with the more sensible definition of valid insertion, we still have
a large number of different valid elaboration strategies. For example, we
may or may not include HM-style let-generalization, as both choices are
valid! It seems to me that implementors must pick specific insertion
strategies, if they want the system to be practical.

In some weak settings, like H-M or predicative System F, it is feasible to
have unique elaboration, because elaboration is "railroaded" by the
restrictions on typing and surface syntax. But if we allow full dependent
types together with first-class implicit function types, we have tremendous
freedom to insert such functions, and I don't think there is anymore a nice
& natural specification of valid insertion, such that elaboration produces
output which is unique with respect to that. Instead, elaboration follows a
particular insertion strategy which is more "algorithmic" than
"declarative".

Nils Anders Danielsson <nad at cse.gu.se> ezt írta (időpont: 2020. aug. 25.,
K, 14:22):

> On 2020-08-25 12:49, András Kovács wrote:
> > 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.
>
> Example:
>
>    id : {A : Set} → A → A
>    id x = x
>
>    f : ?
>    f = id
>
> What is the elaborated right-hand side of f? Is it "id" or
> "id {A = <something>}"?
>
> > 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.
>
> Can you elaborate on this?
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200825/2ce453ba/attachment.html>