<br><div class="gmail_quote">On Tue, Jul 5, 2011 at 3:08 PM, Simon Foster <span dir="ltr"><<a href="mailto:s.foster@dcs.shef.ac.uk">s.foster@dcs.shef.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi,<br>
<br>
A slightly technical question about the Agda core - why do (some?) implicit variables which are applied to a data constructor get converted into anonymous meta-variables when converting from the internal syntax to the abstract syntax? e.g. If I have a function<br>
<br>
++-rzero : ∀ {A : Set} → (xs : List A) → xs ++ [] ≡ xs<br>
<br>
and ask for the type of ++-rzero {A} I get shown<br>
<br>
(x : A) (xs : List A) → _≡_ {List A} (_∷_ {_} x xs) (_∷_ {_} x xs)<br>
<br>
I assume this is down to the "whocares" assignment in InternalToAbstract.hs, because AFAICS the variables are represented explicitly in the internal syntax (i.e. when I do inferExpr on the name of ++-rzero).<br>
</blockquote><div><br></div><div>They're not actually present in the internal syntax. Implicit arguments to functions are stored in the internal syntax, but the datatype parameters are not stored as arguments to constructors. The reason for this is that they are uniquely determined by the type of the constructor application. Of course, we really ought to use that when going back to abstract syntax and put the correct term there.</div>
<div><br></div><div>/ Ulf</div></div>