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.
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
<sjoerd@w3future.com> 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