[Haskell-cafe] Proof in Haskell

[Iavor Diatchki]

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 <aditya.siram at gmail.com> 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 <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
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>