<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Dear Daniel.</p>
<p>In general, intrinsically typed representations are definitely
the way to go when your object language does not have a conversion
relation. <br>
</p>
<p>If your language does have a conversion or judgemental equality
relation, then intrinsic representations are enormously harder to
work with. The basic issue is that the datatype representing
typing will have proof trees corresponding to derivations of
judgemental equality, and quotienting by the derivation of
convertibility is giant PITA. (This is still active research, and
I'm not actually up to date on where the state of the art here is
-- probably Thorsten knows.) <br>
</p>
<p>In your particular case, however, it looks like you have a
different problem. The _._ constructor in your screen shot has the
type: <br>
</p>
<blockquote>
<p><tt>_·_ : ∀{Δ} {Γ₁ Γ₂ : Context Δ} {A B q} <br>
→ Γ₁ ⊢ A -⟨ q ⟩→ B <br>
→ Γ₂ ⊢ A<br>
→ (q ** Γ₂ ++ Γ₁) ⊢ B <br>
</tt></p>
</blockquote>
<p>Here, the return type of the function has an index which has
function calls in it:</p>
<blockquote>
<p><tt> ... → (<b>q ** Γ₂ ++ Γ₁</b>) ⊢ B <br>
</tt></p>
</blockquote>
<p>The Agda type inference algorithm uses unification, and
unification problems involving calls to arbitrary functions are,
in general, hopeless. <b>Unification and pattern match coverage
will generally only work reliably if the return type's indices
contain expressions made only from variables and data
constructors. </b><br>
<b></b></p>
<p>If memory serves, Conor McBride calls indices containing function
calls "green slime", and warns people never to touch it. The way
to keep from being contaminated by green slime is to use an
explicit equality -- if you change your datatype declaration to
the following:<br>
</p>
<blockquote>
<p><tt>_·_ : ∀{Δ} {Γ₁ Γ₂ Θ : Context Δ} {A B q} <br>
→ Γ₁ ⊢ A -⟨ q ⟩→ B <br>
→ Γ₂ ⊢ A<br>
→ Θ ≡ q ** Γ₂ ++ Γ₁<br>
→ Θ ⊢ B <br>
</tt></p>
</blockquote>
The case splitter will see the variable <tt>Θ </tt>and happily
introduce a case for the <tt>_·_ </tt>constructor. But in the case
branch, you will possess the equality <tt>Θ ≡ q ** Γ₂ ++ Γ₁</tt>
which you can use to do any necessary reasoning yourself, thereby
sparing the match coverage algorithm from having to do arbitrary
mathematical reasoning. <br>
<tt></tt>
<p>Best,<br>
Neel<br>
</p>
<div class="moz-cite-prefix">On 01/10/2020 04:48, Daniel Lee wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAJ-vFh9yjO3VF7s0EGAqXvTiDXG2tLCwWtGhYKVHHeJTHyDBwg@mail.gmail.com">
<pre class="moz-quote-pre" wrap="">Hi all,
I'm super new to Agda and the Agda community. Hopefully this is the right
place to ask something like this, but please call me out if it isn't.
I'm working on an Agda development for a QTT formalization. I'm trying to
use an intrinsically typed representation for terms, but run into
unification issues when trying to define substitution.
Substitution:
[image: Screen Shot 2020-09-30 at 8.34.38 PM.png]
Error message:
[image: Screen Shot 2020-09-30 at 8.34.50 PM.png]
Application def:
[image: Screen Shot 2020-09-30 at 8.35.05 PM.png]
I'm sort of at a loss for how to get around this. Is the issue because of
the functions in the return type?
More broadly, it seems like intrinsic typing is the Agda way of doing
things, and gives a lot for free. And it works really well in the STLC
example given in the PLFA textbook. But for a more complicated type system
like this, I'm starting to think it might be easier to use extrinsic
typing? I've also had to rely on the REWRITE pragma which I just learned
isn't allowed in --safe due to potential non-convergence.
Does someone maybe have experience with this and could speak to pros/cons
of using intrinsic vs extrinsic typing here?
Thanks,
Daniel
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre class="moz-signature" cols="72">--
Neel Krishnaswami
<a class="moz-txt-link-abbreviated" href="mailto:nk480@cl.cam.ac.uk">nk480@cl.cam.ac.uk</a></pre>
</body>
</html>