Finding the computational interpretation of a theorem

Question

I have the following theorem: (A→(B→C))→((A∧B)→C), and I am trying to determine what its computational interpretation is. I have the following options:

(1) The function that transforms a curried function to an uncurried one.

(2) The function that transforms an uncurried function to a curried one.

(3) The function that creates a tuple of the two given A values and B values.

(4) There is no computational interpretation of this logical formula.

I don't think that either (1) or (2) are correct since in Haskell, all functions are considered curried. I am thinking that option (3) is correct since (A∧B) is the tuple (A,B) when converted to a type. However, I am not sure whether my reasoning is correct. Is it possible to have a curried function where you take the first two parameters A and B and then somehow convert them into a tuple and then return a value C? Any insights are appreciated.

Answer 1

I don't think that either (1) or (2) are correct since in Haskell, all functions are considered curried.

Here you’re slightly mistaken: all functions written as if they had multiple arguments are implicitly curried, so some function like:

f c n = ord c + n

-- desugared:

f = \ c n -> ord c + n

f = \ c -> \ n -> ord c + n

Has a curried type like Char -> Int -> Int (with a chain of unary functions) rather than an uncurried type (Char, Int) -> Int (a function of multiple arguments, represented in Haskell using a tuple because it has no native notion of multi-argument functions).

(1) is correct because (A→(B→C))→((A∧B)→C) is (a -> (b -> c)) -> ((a, b) -> c) in Haskell types, and we can implement this by iteratively filling in holes.

f = _ :: (a -> (b -> c)) -> ((a, b) -> c)

-- omitting redundant parentheses:

f = _ :: (a -> b -> c) -> (a, b) -> c

f must have a function type:

f = \ g -> _ :: ((a, b) -> c)

The result of f must also be a function, which accepts a tuple:

f = \ g -> \ (x, y) -> _ :: c

Is it possible to have a curried function where you take the first two parameters A and B and then somehow convert them into a tuple and then return a value C?

Sort of, but here I think is where you’ve gotten mixed up—at this point the result of the function returned by f must be of type c, and the only way we can obtain a c is by applying g :: a -> b -> c to x :: a and y :: b. This is because a, b, and c are polymorphic type variables: the caller specifies them, and we know nothing about them within f.

f = \ g -> \ (x, y) -> g x y

-- with some syntactic sugar:

f g = \ (x, y) -> g x y

f g (x, y) = g x y

-- example usage:

> f (+) (1, 2)
3

So f is exactly uncurry, which transforms a curried function to an uncurried one.

Answer 2

(A∧B) is the tuple (A,B) when converted to a type

This is correct. But that doesn't make (A→(B→C))→((A∧B)→C) a “function that creates a tuple of the two given A values and B values”. Such a function would be A→B→(A∧B).

in Haskell, all functions are considered curried

No, that's not quite right. The language itself doesn't define how functions with multiple arguments are expressed. It doesn't have a concept of multiple-argument functions. It's a matter of convention whether to choose to express multiple-argument functions by passing one argument at a time (curried) or by passing tuples (uncurried). These conventions have serious implications on library and compiler design, but from the perspective of the language itself, the choice of currying or not is indifferent.

The computational interpretation of A→(B→C) is a function that takes one argument and returns a function that takes a second argument, i.e. that takes two arguments in curried form. The computational interpretation of (A∧B)→C is a function that takes one argument which is a pair, i.e. that takes two arguments in uncurried form. Therefore the computational interpretation of (A→(B→C))→((A∧B)→C) is a function that transforms a function in curried from into a function in uncurried form.