Does proofs are programs apply to any functional program?

Question

Does Curry howard correspondence, apply to all Functional Program, e.g. in Haskell. i.e. Is it possible to write Equivalent Haskell programs, to COQ proofs?

Answer 1

In Haskell there are more programs than there are Coq proofs because Haskell has general recursion whereas Coq does not. (In fact Coq allows you to extract proofs into Haskell code.)

The reason that Coq does not have general recursion is that with it we can "prove" anything, simply by saying "to prove $t$ just make a recursive call to itself":

proveAnything :: t
proveAnything = proveAnything

In some languages, for instance in OCaml, you can't do it this way so you have to go indirectly through a recursive function call:

let rec proveAnythingAux _ = proveAnythingAux ()
let proveAnything = proveAnythingAux ()

This shows that type theory can be used for many things, two of which are programming and logic. The difference between these two is general recursion: we want it in programming but it makes logic inconsistent.

Answer 2

The Curry-Howard correspond is an observation that the structure of type systems mirrors the structure of logics, specifically propositions. Under this view, we can see similarities between an expression of a certain type, and a proof of a proposition.

Of course, there are many type systems (and logical systems) under the sun, and it is not an exact correspondence. Some type systems are stronger than other. Some languages that call themselves functional don't even have type systems (e.g. Lisp).

Moreover, the mapping is not always intuitive: what does it mean to say that the type of natural numbers is a proposition? It would be more accurate to say that some types can be considered propositions.