Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

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?

share|improve this question

migrated from stackoverflow.com Jun 3 '11 at 11:18

This question came from our site for professional and enthusiast programmers.

Anyone care to explain why the "close" votes, please? –  Grigory Javadyan Jun 1 '11 at 18:53
@Grigory Javadyan: I didn't vote to close, but it's probably because the question is borderline off-topic for SO--philosophical questions, objectively answerable or otherwise, aren't generally appropriate here. In this case I think it's justifiable, though, because the answer has deep practical implications for how Haskell is actually used. –  camccann Jun 1 '11 at 19:24
@Grigory: if this question was a real problem with a real solution (in code) then it can stay on SO. Voted to close and move to Programmers. –  sixlettervariables Jun 2 '11 at 15:32
Just to add to that because I'm a bit steamed up -- the answers to this questions are rife with references to hard CS research and in that sense more "objective" than 90% of SO. Furthermore, sixlettervariable's criteria (that the solution needs code) is insanely narrow for a wide range of genuine programming questions that are neither subjective nor off-topic. I really would hate to see the inclusionist/deletionist debate reemerge on SO, but if clearly programming threads like this get bumped, then I worry... –  sclv Jun 9 '11 at 5:21
I'm ambivalent about where this ends up, mostly because I'm really unclear on what sort of content is supposed to be on Programmers.SE vs. SO. But I will say that Programmers is described in several places as being for "subjective questions", which this question is emphatically not. My answer is about as informal and hand-wavy as it could be and I could still back most of it up easily with references even uptight Wikipedia editors would accept. –  C. A. McCann Jun 15 '11 at 3:01

5 Answers 5

up vote 33 down vote accepted

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.

share|improve this answer

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 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.

share|improve this answer
It might be good to emphasize that nontermination undermines the proof in certain ways that, while obviously catastrophic from a logical standpoint, preserve many other properties. In particular, a function A -> B, given an A, will either produce a B or nothing at all. It will never produce a C, and which value of type B it provides, or if it diverges, still depend exclusively on the A provided. –  camccann Jun 1 '11 at 17:25
@camccann -- a bit nitpicky, but I would distinguish between bottom and "nothing at all", which is more like Void, no? Laziness makes it more and less complicated both. I'd say that a function of A -> B always produces a value of type B, but that value may have less information than one would expect. –  sclv Jun 1 '11 at 22:08
Nitpicking is fun! When I say "nothing" I mean at the value level in a context of performing evaluation, whereas bottom only really exists as an abstraction, not something tangible. An expression being evaluated will never "see" a value of bottom, just terms it doesn't use (which could be bottom) and terms it uses (which have non-bottom values). Trying to use bottom "never happens" in some sense because attempting to do so ends the evaluation of the entire expression before the use would occur. –  camccann Jun 1 '11 at 23:06

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:

*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.

share|improve this answer

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.

share|improve this answer

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.

share|improve this answer
how does this answer the question asked, "what are the noticeable ways in which this statement affected the design of the language? " –  gnat 2 days ago
@gnat - this answer addresses an underlying assumption within the original question, namely: "doesn't this really apply to pretty much all the programming languages?" This answer claims / shows that assumption to be invalid, so it doesn't make sense to address the rest of the questions which are based on a flawed premise. –  GlenH7 yesterday

protected by gnat 2 days ago

Thank you for your interest in this question. Because it has attracted low-quality answers, posting an answer now requires 10 reputation on this site.

Would you like to answer one of these unanswered questions instead?

Not the answer you're looking for? Browse other questions tagged or ask your own question.