I don't know the formal definition, but dependent types seem analogous
to checking an invariant at runtime.
-deech
On Tue, Dec 21, 2010 at 5:53 AM, 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe