[Haskell-cafe] Proof in Haskell
aditya.siram at gmail.com
Tue Dec 21 17:15:56 CET 2010
I don't know the formal definition, but dependent types seem analogous
to checking an invariant at runtime.
On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne <patrick.browne at dit.ie> wrote:
> 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?
>  http://email@example.com/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
More information about the Haskell-Cafe