Currying


portrait of Haskell B. Curry

Haskell Curry studied the relationships between logical proofs and functions. One of his many contributions (independently due to W. Howard) was the "Howard-Curry isomorphism", which states that there is an equivalence between types and logical propositions, where the type A -> B corresponds to the proposition "A implies B", and a function of type A -> B can be seen as mapping proofs of the proposition "A" to proofs of the proposition "B", and is therefore a proof of the proposition "A implies B".

Part of this programme of research involved studying the expressiveness of (effectively) functional programming languages, for which it was useful to strip these languages to the bare bone, and present a minimal functional language in which everything was a function (see the later lectures on the lambda-calculus;). Part of this involves replacing functions of type (A,B) -> C with the equivalent function of type A -> B -> C; if f :: (A,B) -> C, then its curried form is the function defined by

    curriedF x y  =  f (x,y)
(The propositional equivalent of this is that the proposition "A and B imply C" is equivalent to the proposition "A implies that B implies C".)


As an exercise, given a curried function curriedG :: A -> B -> C, how would you define its "uncurried" equivalent g :: (A,B) -> C?


 
Grant Malcolm
Last modified: Fri Nov 2 12:29:25 GMT 2001