[Haskell-cafe] Proof in Haskell

[Patrick Browne]

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