I think it's pretty legit. You aren't actually making a claim about the values in the tree but I think parametricity handles that for you, especially since you have existential types for the payload at every tree level (so you can't go shuffling those around).<div>
<br></div><div>The only thing missing (and that you can't change in Haskell) is that your statement is about Mirror (Mirror x) == x, rather than mirror (mirror x) == x. mirror gives you Mirror but there's currently no proof to show that it's the only way to do it, so there's a missing step there, I think.<br>
<br></div><div>Anyway, for those talking about the coinductive proof, I made one in Agda: <a href="http://hpaste.org/42516/mirrormirror">http://hpaste.org/42516/mirrormirror</a></div><div><br></div><div>Simulating bottoms wouldn't be too hard, but I don't think the statement is even true in the presence of bottoms, is it?</div>
<div><br></div><div>Dan</div><div><br><div class="gmail_quote">On Thu, Dec 23, 2010 at 9:27 AM, Sjoerd Visscher <span dir="ltr"><<a href="mailto:sjoerd@w3future.com">sjoerd@w3future.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im"><br>
On Dec 21, 2010, at 6:57 PM, austin seipp wrote:<br>
<br>
> <a href="https://gist.github.com/750279" target="_blank">https://gist.github.com/750279</a><br>
<br>
</div>I took Austins code and modified it to run on a Tree GADT which is parameterized by its shape:<br>
<br>
<a href="https://gist.github.com/752982" target="_blank">https://gist.github.com/752982</a><br>
<br>
Would this count as a function mirror with proof that mirror (mirror x) == x?<br>
<br>
--<br>
<font color="#888888">Sjoerd Visscher<br>
</font><div><div></div><div class="h5"><br>
<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div>