"A proof is a program; the formula it proves is a type for the program"

Question

This might be a philosophical kind of question, but I believe that there is an objective answer to it.

If you read the wikipedia article about Haskell, you can find the following:

The language is rooted in the observations of Haskell Curry and his intellectual descendants, that "a proof is a program; the formula it proves is a type for the program"

Now, what I'm asking is: doesn't this really apply to pretty much all the programming languages? What feature (or set of features) of Haskell makes it compliant with this statement? In other words, what are the noticeable ways in which this statement affected the design of the language?

Answer 1

The essential concept applies universally in some fashion, yes, but rarely in a useful manner.

To start with, from the type theory perspective this assumes, "dynamic" languages are best regarded as having a single type, which contains (among other things) metadata about the nature of the value the programmer sees, including what these dynamic languages would call a "type" themselves (which is not the same thing, conceptually). Any such proofs are likely to be uninteresting, so this concept is mostly relevant to languages with static type systems.

Additionally, many languages that allegedly have a "static type system" must be regarded as dynamic in practice, in this context, because they permit inspection and conversion of types at run-time. In particular, this means any language with built-in, by-default support for "reflection" or such. C#, for instance.

Haskell is unusual in how much information it expects a type to provide--in particular, functions cannot depend on any value other than the ones specified as its arguments. In a language with mutable global variables, on the other hand, any function can (potentially) inspect those values and change behavior accordingly. So a Haskell function with type A -> B can be regarded as a miniature program proving that A implies B; an equivalent function in many other languages would only tell us that A and whatever global state is in scope combined imply B.

Note that while Haskell does have support for things like reflection and dynamic types, use of such features must be indicated in the type signature of a function; likewise for use of global state. Neither is available by default.

There are ways to break things in Haskell as well, e.g. by allowing runtime exceptions, or using non-standard primitive operations provided by the compiler, but those come with a strong expectation that they will only be used with full understanding in ways that won't damage the meaning of external code. In theory the same could be said of other languages, but in practice with most other languages it is both more difficult to accomplish things without "cheating", and less frowned-upon to "cheat". And of course in true "dynamic" languages the whole thing remains irrelevant.

The concept can be taken much further than it is in Haskell, as well.

Answer 2

You're correct that the Curry-Howard correspondence is a very general thing. It's worth familiarizing yourself with a bit on its history: http://en.wikipedia.org/wiki/Curry-Howard_correspondence

You'll note that as originally formulated, this correspondence applied particularly to intuitionistic logic on the one side, and the simply typed lambda calculus (STLC) on the other.

Classic Haskell -- either '98 or even earlier versions, hewed very closely to the STLC, and for the most part there was a very simple, direct translation between any given expression in Haskell and a corresponding term in the STLC (extended with recursion and a few primitive types). So this made Curry-Howard very explicit. Today, thanks to extensions, such a translation is a somewhat more tricky business.

So in a sense, the question is why Haskell "desugars" into the STLC so straightforwardly. Two things come to mind:

• Types. Unlike Scheme, which is also a sugared lambda calculus of sorts (among other things), Haskell is strongly typed. This means that there do not exist terms in classic Haskell which by definition cannot be well typed terms in the STLC.
• Purity. Again, unlike Scheme, but like the STLC, Haskell is a pure, referentially transparent, language. This is quite important. Languages with side-effects can be embedded into languages which are side-effect free. However, doing so is a whole-program transformation, not simply a local desugaring. So to have the direct correspondence, it is necessary that you begin with a purely functional language.

There is also an important way in which Haskell, like most languages, fails with regards to a direct application of the Curry-Howard correspondence. Haskell, as a turing-complete language, contains the possibility of unlimited recursion, and hence of non-termination. The STLC does not have a fixpoint operator, is not turing-complete, and is strongly normalizing -- which is to say that no reduction of a term in the STLC will fail to terminate. The possibility of recursion means that one can "cheat" Curry-Howard. For example, let x = x in x has the type forall a. a -- i.e., since it never returns, I can pretend it gives me anything! Since we can always do this in Haskell, that means that we can't "believe" fully in any proof corresponding to a Haskell program unless we have a separate proof that the program itself is terminating.

The lineage of functional programming prior to Haskell (notably the ML family) was a result of CS research focused on building languages that you could easily prove things about (among other things), research very much aware of and stemming from CH to begin with. Conversely, Haskell has served as both a host-language and an inspiration for a number of proof assistants under development, such as Agda and Epigram, which are rooted in developments in type theory very much related to the lineage of CH.

Answer 3

To a first-order approximation, most other (weakly and/or uni-typed) languages do not support the strict language-level delineation between a

• proposition (i.e. a type)
• a proof (i.e. a program demonstrating how we can construct the proposition from a set of primitives and/or other higher order constructs)

and the strict relation between the two. If anything, the best guarantees other such languages provide are

• given a limited constraint on the input, along with whatever happens to be in the environment at the time, we can produce a value with a limited constraint. (traditional static types, c.f. C/Java)
• every construct is of the same type (dynamic types, c.f. ruby/python)

Note that by type, we refer to a proposition, and hence something describing far more information then merely int or bool. In Haskell, there is a permeating culture of a function is only affected by it's arguments - no exceptions*.

To be a tad bit more rigorous, the general idea is that by enforcing a rigid intuitionistic approach to (nearly) all program constructs (i.e. we can only prove that which we can construct), and by limiting the set of primitive constructs in such a way that we have

• strict propositions for all language primitives
• a limited suite of mechanisms by which primitives may be combined

Haskell constructions tend to lend themselves very well to reasoning about their behaviour. If we can construct a proof (read: function) proving that A implies B, this is has very useful properties:

• it always holds (as long as we have an A, we can construct a B)
• this implication relies only on A, and nothing else.

thus allowing us to reason about local/global invariants effectively. To get back to the original question; Haskell's language features that best fascilitate this mindset are:

• Purity/Segmentation of effects into explicit constructs (effects are both accounted for and are typed!)
• Type Inference/Checking in Haskell compilers
• The ability to embed control and/or data flow invariants into the propositions/types a program is setting out to prove: (with Polymorphism, Type Families, GADT's etc.)
• Referential Integrity

None of which are at all unique to Haskell (many of these ideas are incredibly old). However, when combined together with a rich set of abstractions in the standard libraries (usually found in type classes), various syntax-level sugaring and a strict commitment to purity in program design, we end up with a language that somehow manages to be both practical enough for real world applications, but at the same time proves easier to reason about then most traditional languages.

This question merits a sufficiently deep answer, and I could not possibly do it justice in this context. I'd suggest reading up more on wikipedia/in the literature:

• The Curry-Howard Isomorphism
• The Lambda Cube
• Constructivist/Intuitionistic Type Theory
• Bob Harper's Overview of Computational Trinitarianism

*NB: I'm glossing over/ignoring some of the trickier aspects of Haskell's impurities (exceptions, non-termination etc.) that would only complexify the argument.

Answer 4

What feature? The type system (being static, pure, polymorphic). A good starting point is Wadler's "Theorems for Free". Noticeable effect on the design of the language? The IO type, type classes.

Answer 5

The Kleene Hierarchy shows us that proofs are not programs.

The first recursive relation is either:

R1( Program , Iteration )  Program halts at Iteration.
R2( Theorem , Proof ) Proof proves a Theorem.

The first recursively enumerable relations are:

(exists x) R1( Program , x )  Program Halts.
(exists x) R2( Theorem , x)   Theorem is provable.

So that a program is a theorem and the iteration that exists at which the program halts is like the proof that exists that proves the theorem.

Program = Theorem
Iteration = Proof

When a program is correctly produced from a specification, we must be able to prove that it satisfies the specification, and if we can prove a program satisfies a specification then it is correct program synthesis. So we perform program synthesis iff we prove the program satisfies the specification. The theorem that the program satisfies the specification is the program in that the theorem refers to the program that is synthesized.

Martin Lof's false conclusions have never produced any computer programs and it is amazing that people believe it is a program synthesis methodology. No complete examples have ever been given of a program being synthesized. A specification such as "input a type and output a program of that type" is not a function. There are multiple such programs and to choose one randomly is not a recursive function or even a function. It is just a silly attempt to show program synthesis with a silly program that does not represent a real computer program calculating a recursive function.