[Haskell-cafe] Proof in Haskell

[aditya siram]

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.browne at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>