It is not possible at the value level, because Haskell does not support dependent types and thus cannot express the type of the proposition "forall a . forall x:Tree a, mirror (mirror x) = x", and therefore a proof term also cannot be constructed.
However, if you manage to express those trees at type level, probably with typeclasses and type families, you might have some success. 2009/9/25 pat browne <patrick.bro...@comp.dit.ie>: > Hi, > Below is a function that returns a mirror of a tree, originally from: > > http://www.nijoruj.org/~as/2009/04/20/A-little-fun.html > > where it was used to demonstrate the use of Haskabelle(1) which converts > Haskell programs to the Isabelle theorem prover. Isabelle was used to > show that the Haskell implementation of mirror is a model for the axiom: > > mirror (mirror x) = x > > My question is this: > Is there any way to achieve such a proof in Haskell itself? > GHC appears to reject equations such has > mirror (mirror x) = x > mirror (mirror(Node x y z)) = Node x y z > > > Regards, > Pat > > > =================CODE===================== > module BTree where > > data Tree a = Tip > | Node (Tree a) a (Tree a) > > mirror :: Tree a -> Tree a > mirror (Node x y z) = Node (mirror z) y (mirror x) > mirror Tip = Tip > > (1)Thanks to John Ramsdell for the link to Haskabelle: > http://www.cl.cam.ac.uk/research/hvg/Isabelle/haskabelle.html). > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe