<div dir="ltr">> What is the elaborated right-hand side of f? Is it "id" or<br>"id {A = <something>}"?<br><div><br></div><div>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.</div><div><br></div><div>> Can you elaborate on this?</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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". </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>> ezt írta (időpont: 2020. aug. 25., K, 14:22):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2020-08-25 12:49, András Kovács wrote:<br>
> However, this uniqueness is only about unification, but that's just<br>
> one part of elaboration. There is also a degree of freedom in deciding<br>
> where to insert implicit applications and lambdas, and Agda's choice<br>
> of insertions is not really unique.<br>
<br>
Example:<br>
<br>
   id : {A : Set} → A → A<br>
   id x = x<br>
<br>
   f : ?<br>
   f = id<br>
<br>
What is the elaborated right-hand side of f? Is it "id" or<br>
"id {A = <something>}"?<br>
<br>
> In general, I think it's practically realistic to have unification<br>
> which produces unique solutions, but not that realistic to have<br>
> elaboration which produces unique output.<br>
<br>
Can you elaborate on this?<br>
<br>
-- <br>
/NAD<br>
</blockquote></div>