<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Related (I hope) to the discussion of eliminators, I want to point
out that if we were working in a type theory based on positive
recursive types rather than primitive datatypes, this example would
not go through (of course).<br>
<br>
Empty := mu X.X<br>
<br>
Box := mu X. (Empty -> X)<br>
<br>
Note that X occurs positively in the body of the mu-type for Box.
The theory gives us a recursor R with this typing rule<br>
<br>
b : Box<br>
f : (Empty -> T) -> T<br>
---------------------<br>
R(b,f) : T<br>
<br>
We certainly have the isomorphism Box = (Empty -> Box) -- it is
even a definitional equality! -- but we cannot use this recursor to
write a term of type Box -> Empty. The best we could do would be
to start like this, where g has type Empty -> Empty, and hence is
useless for deriving Empty.<br>
<br>
loop = \ b . R(b, \ g . (g ?))<br>
<br>
So I think the wrap constructor being used in Maxime's code is just
an explicit witness of the above implicit isomorphism. Removing it
should not count for structural decrease (obviously).<br>
<br>
Cheers,<br>
Aaron<br>
<br>
<div class="moz-cite-prefix">On 01/08/2014 11:53 AM, Andreas Abel
wrote:<br>
</div>
<blockquote cite="mid:52CD90B4.40804@ifi.lmu.de" type="cite">
<pre wrap="">Conor,
that's on the latest darcs version of Agda, I guess?
At least my own version of --without-K rejects your match on Refl:
The indices
WOne
X
are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)
when checking that the pattern Refl has type WOne <-> X
But you say it is justified, is it?
Cheers,
Andreas
On 07.01.2014 17:42, Conor McBride wrote:
</pre>
<blockquote type="cite">
<blockquote type="cite">
<pre wrap="">Very good. Agda is right and Coq got it wrong. As I said previosuly the
definition of loop implicitely uses K.
</pre>
</blockquote>
<pre wrap="">
Not so fast! The code below is accepted using the --without-K flag, and
the elimination that noo does is a based path induction, IIUC.
Conor
{-# OPTIONS --without-K #-}
module BadWithoutK where
data Zero : Set where
data WOne : Set where
wrap : (Zero -> WOne) -> WOne
data _<->_ (X : Set) : Set -> Set where
Refl : X <-> X
postulate
myIso : WOne <-> (Zero -> WOne)
moo : WOne -> Zero
noo : (X : Set) -> (WOne <-> X) -> X -> Zero
moo (wrap f) = noo (Zero -> WOne) myIso f
noo .WOne Refl x = moo x
bad : Zero
bad = moo (wrap \ ())
</pre>
</blockquote>
<pre wrap="">
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<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://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>