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).
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.
Anyway, for those talking about the coinductive proof, I made one in Agda:
http://hpaste.org/42516/mirrormirror
Simulating bottoms wouldn't be too hard, but I don't think the statement is
even true in the presence of bottoms, is it?
Dan
On Thu, Dec 23, 2010 at 9:27 AM, Sjoerd Visscher
On Dec 21, 2010, at 6:57 PM, austin seipp wrote:
I took Austins code and modified it to run on a Tree GADT which is parameterized by its shape:
https://gist.github.com/752982
Would this count as a function mirror with proof that mirror (mirror x) == x?
-- Sjoerd Visscher
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe