[Haskell-cafe] Proof in Haskell
patrick.browne at dit.ie
Tue Dec 21 12:53:36 CET 2010
In a previous posting 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
>> "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?
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
More information about the Haskell-Cafe