<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<tt>Hi all,<br>
<br>
This is indeed the right move. An additional trick one can play is
to<br>
use an *inductive* 4-place </tt><tt><tt>relation `Θ ≡ q ** Γ₂ ++
Γ₁` instead of a mere<br>
equality proof. With this extra structure, you will be able to
perform<br>
induction directly on the proof rather than having to do case
analysis<br>
on `</tt></tt><tt><tt><tt>Θ` and `Γ₂` and use the proof of
equality to dismiss the impossible<br>
cases. This should make the whole experience more pleasant.<br>
<br>
Best,<br>
gallais<br>
<br>
<br>
</tt></tt></tt>
<div class="moz-cite-prefix">On 01/10/2020 09:44, Neel Krishnaswami
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:12cc95ae-b65b-e89a-1f52-893533175a87@cl.cam.ac.uk">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<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>
</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>
<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" moz-do-not-send="true">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7Cec25fc40f26f43e1903108d865e62ade%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637371386947887249&sdata=J5IxVSpywjzqZdwaL%2Fzl7TGE3V%2B5lhLJfBo11IoUvbY%3D&reserved=0" originalsrc="https://lists.chalmers.se/mailman/listinfo/agda" shash="wELiWXsvklA7fXNTOFE9V7edeaGMgfHDZ8kL/ES8zHbNEbqQ55F5YnDoLcfZ3a5mtiADUz0WVXePwG1gJqi0BuuxqExJXQ2B7u7jTQx2dRGSMb2THJLm/1nC5UOOqjNw1MiMtcDwrucG2mUZfaZ9FlzqFTG4YeQHd0ki9HbvkVs=" moz-do-not-send="true">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" moz-do-not-send="true">nk480@cl.cam.ac.uk</a></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://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7Cec25fc40f26f43e1903108d865e62ade%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637371386947907230&sdata=%2FZY4zKWoYjDwh0yDY%2BO0S76IWk9WC5caow98WgTuBxw%3D&reserved=0">https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7Cec25fc40f26f43e1903108d865e62ade%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637371386947907230&sdata=%2FZY4zKWoYjDwh0yDY%2BO0S76IWk9WC5caow98WgTuBxw%3D&reserved=0</a>
</pre>
</blockquote>
<br>
</body>
</html>