Curry-Howard Isomorphism

The expression Curry-Howard isomorphism is much used in theoretical computer science[?], to express an important underlying principle connecting the adjacent areas of lambda calculus and type theory. It is an almost complete misnomer (in a grand tradition of mathematics), since the formulation isn't Haskell Curry's, and the content isn't from a pedantic point of view an isomorphism.

Starting from the point of view that functional programming supports programming languages that are typed and have higher-order functions, the primary content of the 'isomorphism' is to identify that amount of structure with that occurring in type theories of intuitionistic logic. Under the influence of category theory there are a number of heuristic ways of looking at the overall position.

A favourite formulation is 'propositions as types'. This is rather more confusing than the matching statement 'proofs as programs': using the idea of category in its very simple form, we can say that if proofs and programs are two kinds of morphisms, then propositions and types are going to be two corresponding kinds of objects. It is suggested that we have two distinct categories, with some sort of functor (translation) from one to the other, respecting structure. This schematic picture at least allows to orient ourselves. We suppose that proofs are here being treated as some sort of high-level programming language, and our functor is acting as a compiler. If we ask 'proofs of what?' the answer is 'of some 'propositions; as proofs carry over to programs, the labelling of propositions becomes that of abstract types. To say we have a functor is to say that modus ponens in some form becomes composition of functional programs, i.e. explicit substitution, operationally speaking.

This is a helpful if schematic guide, that will apply over a range of situations. That is, we don't expect there to be a single, canonical formulation. A traditional way of looking at it is to expect existentially quantified propositions to lead (in intuitionistic logic) to constructive solutions of problems posed. This goes back to Kolmogorov, and fits perfectly with the category theory view. With emphasis at the morphism level, we interpret A implies B as a function-space type: if A says something exists satisfying P, and B that something exists satisfying Q, then our interest is in methods that construct something of type Q from something of type P (Kolmogorov's interpretation). That this matches up on the functional program side is the basic identification of cartesian-closed categories[?] as the models for typed lambda-calculus.

In this way the content of the Curry-Howard isomorphism can practically be integrated into categorical logic[?], as foundational explanation of the modelling. Type theories become categories, categories support lambda calculus interpretations. The programming content is perhaps concealed, in the next step of compiling lambda calculus into something lower-level (provided by Curry's combinatory logic). Whether it should so be read is of course another matter. There are other heuristics, such as the universal quantifier interpretation of the function space (as converting one proposition with an existential quantifier to another).