[Haskell-cafe] Proof in Haskell

[Daniel Peebles]

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 <sjoerd at w3future.com>wrote:

>
> On Dec 21, 2010, at 6:57 PM, austin seipp wrote:
>
> > https://gist.github.com/750279
>
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20101223/2988fd44/attachment.htm>