<div dir="ltr"><div>Well, if we don't have strong normalization we also lose decidability of typechecking, which is kind of an important design goal of Agda IMO.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, May 1, 2019 at 12:17 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div lang="EN-GB">
<div class="gmail-m_-3192465064702660474WordSection1">
<p class="MsoNormal">I am just wondering with normalisation under inconsistent assumptions is such an important feature? Is this the only thing that goes wrong?<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Thorsten<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<div style="border-color:rgb(181,196,223) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12pt;color:black">From: </span></b><span style="font-size:12pt;color:black">Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>><br>
<b>Date: </b>Wednesday, 1 May 2019 at 08:48<br>
<b>To: </b>Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" target="_blank">matthewdaggitt@gmail.com</a>><br>
<b>Cc: </b>Agda mailing list <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>Re: [Agda] Pattern matching on irrelevant types with only one constructor?<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">Hi Matthew,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">In our paper on definitional proof irrelevance (<a href="https://hal.inria.fr/hal-01859964" target="_blank">https://hal.inria.fr/hal-01859964</a>) we give a criterion for when it is allowed to pattern match on an irrelevant argument. As we argue in the
paper, the condition that the datatype has a single constructor is neither sufficient nor necessary. The criterion we give is not yet implemented in Agda, but I hope to add it in the not-too-distant future (it depends on my PR
<a href="https://github.com/agda/agda/pull/3589" target="_blank">https://github.com/agda/agda/pull/3589</a> being merged first). Unfortunately, the Acc datatype does not satisfy this criterion. In fact, allowing pattern matching on irrelevant Acc would break strong normalization
of the theory, as you can always have an absurd hypothesis of type Acc but evaluation would not be blocked on this argument because it's irrelevant. So the best you can do is get propositional (instead of definitional) irrelevance by proving irrelevance of
Acc by hand (or postulate it).<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">A historical note: Agda used to allow matching on single-constructor datatypes under the --experimental-irrelevance flag, but this was completely broken so I decided to remove it last year (<a href="https://github.com/agda/agda/commit/b5f8b509bbe362c4bbb14612a6666e720cabf26a" target="_blank">https://github.com/agda/agda/commit/b5f8b509bbe362c4bbb14612a6666e720cabf26a</a>)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">-- Jesper<u></u><u></u></p>
</div>
</div>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">On Wed, May 1, 2019 at 8:33 AM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" target="_blank">matthewdaggitt@gmail.com</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-color:currentcolor currentcolor currentcolor rgb(204,204,204);border-style:none none none solid;border-width:medium medium medium 1pt;padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal"> In the Agda <a href="https://agda.readthedocs.io/en/v2.6.0/language/irrelevance.html" target="_blank">
documentation</a> it is pretty clear that the only time you can pattern match against irrelevant arguments is when the type is empty. My own reasoning for this has always been that this is to stop decisions being made depending on the result of the pattern
match. This leads me to wonder if there are any theoretical reasons why it's not possible to also mark a type irrelevant when it only has a single constructor?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Consider the motivating example below. Clearly the `Acc` argument is never actually used in the computation of the final value, and no decisions can be based on its value as it only has a single constructor. It seems like it should be possible
to mark it irrelevant. If this were possible then we would immediately get rid of a whole bunch of annoying congruence lemmas.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">```<u></u><u></u></p>
<div>
<p class="MsoNormal">gcd : (m n : <span style="font-family:"Cambria Math",serif">
ℕ</span>) → Acc _<_ m → n < m → <span style="font-family:"Cambria Math",serif">ℕ</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">gcd m zero _ _ = m<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">gcd m (suc n) (acc rec) n<m = gcd′ (suc n) (m % suc n) (rec _ n<m) (a%n<n m n)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">```<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Many thanks,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Matthew<u></u><u></u></p>
</div>
</div>
</div>
<p class="MsoNormal">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><u></u><u></u></p>
</blockquote>
</div>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</pre></div>
</blockquote></div>