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/[email protected]/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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
