<div dir="ltr"><div class="gmail_extra">On Wed, Jan 8, 2014 at 9:41 PM, Conor McBride <span dir="ltr"><<a href="mailto:conor@strictlypositive.org" target="_blank">conor@strictlypositive.org</a>></span> wrote:<br><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div class="im"><br>
</div>One reason why my brief career as a singer-songwriter was curtailed is that<br>
I could never remember the words, but I think it highly unlikely that the<br>
paper we wrote back then made any kind of assurance about mutual definitions<br>
like moo and noo. If I did, then perhaps I join the good company in error,<br>
for which I apologize.<br></blockquote><div><br></div><div style>I'm sorry, I meant the version of noo I gave in my previous mail. I'd better call it something else:</div><div style><br></div><div style><div class="im" style="font-family:arial,sans-serif;font-size:13px">
woo : (X : Set) -> (WOne <-> X) -> X -> Zero<br></div><span style="font-family:arial,sans-serif;font-size:13px">woo .WOne Refl (wrap f) = woo (Zero -> WOne) myIso f</span><br style="font-family:arial,sans-serif;font-size:13px">
</div><div style><span style="font-family:arial,sans-serif;font-size:13px"><br></span></div><div style><div><font face="arial, sans-serif">bad : Zero</font></div><div><font face="arial, sans-serif">bad = woo WOne Refl (wrap \ ())</font></div>
</div><div style><span style="font-family:arial,sans-serif;font-size:13px"><br></span></div><div style><span style="font-family:arial,sans-serif;font-size:13px">The definition of woo falls within the framework of EDPM. Moreover, it is structurally recursive on its third argument. It is still incompatible with univalence (as shown by 'bad'), and it cannot be translated to eliminators.</span></div>
<div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
I quite agree that the definition of "structurally smaller" we gave does say<br>
that<br>
<br>
f < wrap f<br>
<br>
where f amounts to a collections of (no) things, all of which are smaller<br>
than (wrap f). NOWHERE is it said that transporting f with respect to an<br>
equation on types respects structural ordering relations, and ESPECIALLY<br>
IN THE PRESENCE OF UNIVALENCE that is OBVIOUS NONSENSE.<br></blockquote><div><br></div><div style>Of course, transporting a term along an equation should not preserve structural ordering. Yet we should still be able to pattern match on equality proofs (in the --without-K sense), as long as the definition can be translated to eliminators.</div>
<div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Eliminators are ok because they fix the "view" of the datatype for the<br>
whole of the recursion. They don't allow you to make up spurious,<br>
allegedly smaller, elements of the type by shipping stuff across<br>
isomorphisms.<br></blockquote><div><br></div><div style>I agree, and I think neither should pattern matching let us do this (at least not with --without-K enabled). But wasn't the whole point of EDPM to show that it *is* safe to use pattern matching? What <span style="font-family:arial,sans-serif;font-size:13px">Daniel and Thomas on the Coq list showed, is that we need an additional criterion for pattern matching to be safe. My proposal is to require that the type of the argument on which the function is structurally recursive, should be a data type. A different (and probably much more sophisticated) proposal was given on the Coq list. Do you have another proposal?</span></div>
<div style><span style="font-family:arial,sans-serif;font-size:13px"><br></span></div><div style><font face="arial, sans-serif">On the long term, I think the best way to go would be to actually perform the translation of pattern matching to eliminators in Agda, similar to Matthieu's Equations plugin for Coq. There are just too many subtleties to pattern matching to get everything correct otherwise, especially when univalence and higher inductives are involved.</font></div>
<div style><span style="font-family:arial,sans-serif;font-size:13px"><br></span></div><div style><span style="font-family:arial,sans-serif;font-size:13px">Jesper</span></div></div></div></div>