[Haskell-cafe] Proof in Haskell

[Eugene Kirpichov]

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.Browne at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru