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 <patrick.bro...@dit.ie> wrote: > 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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe