<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<br>
<div class="moz-cite-prefix">Le 09/01/2014 01:14, Jesper Cockx a
écrit :<br>
</div>
<blockquote
cite="mid:CAEm=bowpVPDwRtssiLwjzH0L0hNEmKQqQacr2owwG9uXQJ0V7Q@mail.gmail.com"
type="cite">
<div dir="ltr">
<div class="gmail_extra">On Wed, Jan 8, 2014 at 9:41 PM, Conor
McBride <span dir="ltr"><<a moz-do-not-send="true"
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>
</div>
</div>
</blockquote>
Hello.<br>
<br>
Note that this condition does not seem to appear in Thierry's
original paper on pattern-matching in MLTT (1992). However, and
sorry for having to cite myself, but I always required such a
condition on my works on the termination of rewriting (which
generalizes pattern-matching) in the calculus of constructions (with
or without sized types). See for instance Def 24 in "Definitions par
rewriting in the calculus of constructions" (Math. Structures in
Comp. Science 15(1), 2005).<br>
<br>
Best regards,<br>
<br>
Frédéric.<br>
<br>
<blockquote
cite="mid:CAEm=bowpVPDwRtssiLwjzH0L0hNEmKQqQacr2owwG9uXQJ0V7Q@mail.gmail.com"
type="cite">
<div dir="ltr">
<div class="gmail_extra">
<div class="gmail_quote">
<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>
</blockquote>
<br>
</body>
</html>