Hi, In a previous posting[1] I asked was there a way to achieve a proof of mirror (mirror x) = x in Haskell itself. The code for the tree/mirror is below: 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 The reply from Eugene Kirpichov was:
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.
Could anyone explain what *dependent types* mean in this context? What is the exact meaning of forall a and forall x? Thanks, Pat [1] http://www.mail-archive.com/haskell-cafe@haskell.org/msg64842.html This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie