Hi Patrick, Indeed, you cannot really write proofs in Haskell because it is just an ordinary (more or less) programming language and not a theorem prover. (As an aside: you could write "tests", i.e. properties which may or may not be theorems about your program, and test them on random data (see QuickCheck), or exhaustively---if you managed to test a property for all possible inputs, then you have essentially proved it.).
Now about dependent types. Some programming languages have very expressive type systems (even more so then Haskell!) and they allow for types which are parameterized by values. Such types are called "dependent types". Here is an example: decrement :: (x :: Int) -> (if x > 0 then Int else String) decrement x = if x > 0 then x - 1 else "Cannot decrement" This function maps values of type "Int" to either "Int"s or "String"s. Note that the _type_ of the result of the function depends on the _value_ of the input, which is why this function has a dependent type. It turns out---and this is not at all obvious at first---that languages with dependent types (and some other features) are suitable not only for writing programs but, also, for proving theorems. Theorems are expressed as types (often, dependent types), while proofs are programs inhabiting the type of the theorem. So, "true" theorems correspond to types which have some inhabitants (proofs), while "false" theorems correspond to empty types. The correspondence between "proofs-theorems" and "programs-types" is known as the Curry-Howard isomorphism. Examples of some languages which use depend types are Coq, Agda, and Cayenne. I hope that this helps, -Iavor PS: The "forall"s in your example are just depend function types: in this setting, to prove "forall (x :: A). P x" amounts writing a function of type: "(x :: A) -> P x". In other words, this is a function, that maps values of type "A" to proofs of the property. Because the function can be applied to any value of type "A", we have prove the result "forall (x::A). P x)". The dependent type arises because the property depends on the value in question. On Tue, Dec 21, 2010 at 8:15 AM, aditya siram <[email protected]> wrote: > 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 <[email protected]> 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/[email protected]/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 >> [email protected] >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > > _______________________________________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
