<div dir="ltr"><div>Hi Peter,</div><div><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><span class="gmail-im"></span>
Interesting.  Would it be right to say that coverage checking <br>
is simple in comparison to termination checking <br>
(which is after all undecidable, in principle)? <br>
</div></blockquote><div><br></div><div>In general, coverage checking is just as undecidable as termination checking, because it requires checking emptiness of a given type to determine whether a case can be omitted. Agda uses inaccessible patterns to recover a decidable fragment of coverage, which is similar to using a particular criterion for termination like structural descent or size-change termination.</div><div></div><div><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
This brought something to mind. With many datatypes (not codata) there<br>
is a canonical eliminator. You could press a button to have it<br>
generated and type-checked for you.  (This might even be useful).<br>
Imaginably, you might also get the canonical anamorphism from<br>
a declaration of codata; or even fancier gadgetry.</blockquote></div><div><br></div><div>It should be possible to use Agda's reflection machinery to write a macro that automatically generates the eliminator for a given datatype (in a certain subset of all datatypes supported by Agda), and similarly you could generate general principles to work with coinductive types like you mention.</div><div></div><div><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
A masochist or an idiot or a compiler from user syntax <br>
might try to write all programs using just these canonical<br>
eliminators as the only source of structural induction and/or recursion, even<br>
case-splits.</blockquote></div><div><br></div><div>The translation from dependent pattern matching to eliminators is automated in the Equations plugin for Coq, so there is no need for masochism. A true masochist could try to reimplement Equations as an Agda macro. Personally I would be more interested to do such a project using a type-safe reflection interface such as levitation. But even with such an automatic translation, I would suspect that you still want to keep around the case tree representation of the function, for efficient evaluation if nothing else.</div><div><br></div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
It seems that there is something like ex-falso-quodlibet<br>
lurking in the corners of full pattern matching. </blockquote></div><div><br></div><div>It makes use of the conflict rule from Conor's "constructions on constructors" to eliminate impossible cases, is this what you meant?<br></div><div></div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Dec 5, 2019 at 2:25 PM Peter Hancock <<a href="mailto:hancock@fastmail.fm" target="_blank">hancock@fastmail.fm</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">On 04/12/2019 09:13, Jesper Cockx wrote:<br>
<br>
> However, this story is far from complete because it takes the signature of<br>
> defined types and functions for granted. In particular, functions by<br>
> dependent pattern matching are represented as case trees that need to pass<br>
> coverage checking and termination checking, which means those checks are<br>
> also part of Agda's 'trusted core'. <br>
<br>
Interesting.  Would it be right to say that coverage checking <br>
is simple in comparison to termination checking <br>
(which is after all undecidable, in principle)? <br>
<br>
This brought something to mind. With many datatypes (not codata) there<br>
is a canonical eliminator. You could press a button to have it<br>
generated and type-checked for you.  (This might even be useful).<br>
Imaginably, you might also get the canonical anamorphism from<br>
a declaration of codata; or even fancier gadgetry.<br>
<br>
A masochist or an idiot or a compiler from user syntax <br>
might try to write all programs using just these canonical<br>
eliminators as the only source of structural induction and/or recursion, even<br>
case-splits.  That might be something like a core language, or <br>
imaginable (if sometimes nasty/prolix) "assembly code".<br>
<br>
One advantage of full pattern matching is avoiding <br>
programs with piles of deeply nested case distinctions.<br>
An example is a proof of transitivity, where<br>
pattern matching allows<br>
<br>
    tr tr' : (a b c : fm) -> Tr a b c<br>
    tr in0 in0 in0 in0* = id   <br>
    tr (inS z) (inS z') (inS z'') (inS* z z' ab) (inS* z' z'' bc)<br>
     = inS* z z'' (tr z z' z'' ab bc)<br>
<br>
The (20 line) proof using just canonical eliminators took me <br>
horribly many hours to figure out. It is computationally horrible.<br>
It works only because the last clause of Tr is an equation.<br>
<br>
It seems that there is something like ex-falso-quodlibet<br>
lurking in the corners of full pattern matching. <br>
To be in a core-language, I wonder if it should be spelled<br>
out by explicitly using a boolean universe, or something ...<br>
<br>
Hank<br>
_______________________________________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>