How is the direct product of the functions (A -> B) * (C -> D) equivalent to the function (A * C) -> (B * D)? Is there an error here?

Question

In the simply typed lambda calculus we have type algebra - types can be added, multiplied and exponentiated, where addition corresponds to the sum type, multiplication to the product type, and functions to the exponential type (where A -> B corresponds to B^A). Due to the commutativity and associativity of the sum type and product type, we will consider such types isomorphic up to a permutation, for example, A * B * C * D * E and C * E * B * A * D can be considered isomorphic.

For example, for any type T, the function type from 0 (void type) to T contains exactly one function, because T ^ 0 = 1. Currying works because nested returns of functions like A -> (B -> (C -> (D -> R))) corresponds to (((R ^ D) ^ C) ^ B) ^ A, which can be converted to R ^ (A * B * C * D), i.e. (A * B * C * D) -> R. Intuitively, a "nullary" function returning a term of type T is equivalent to a term of type T itself. A nullary function can also be thought of as a function that takes an empty product type, i.e. 1 (unit type), which is completely consistent with the type algebra, because 1 -> T corresponds to T ^ 1 = T, i.e. there are as many nullary functions returning a term of type T as there are terms of type T themselves.

In some sources, I have seen expressions like (A + B) -> C = (A -> C) * (B -> C), which is completely valid, because C ^ (A + B) = (C ^ A) * (C ^ B), as well as A -> (B * C) = (A -> B) * (A -> C), which is also completely valid, since (B * C) ^ A = (B ^ A) * (C ^ A). However, in the same sources, I also came across the expression (A -> B) * (C -> D) (i.e. the type of all tuples of functions from A to B and from C to D) = (A * C) -> (B * D) (i.e. the type of all functions from a tuple of A and C to a tuple of B and D). But in general case (B ^ A) * (D ^ C) =/= (B * D) ^ (A * C)! In other words, the number of elements of type (A -> B) * (C -> D) in general case may differ from the number of elements of type (A * C) -> (B * D).

It's some kind of mistake or I'm not understanding something?

Thanks in advance.

Answer 1

You are correct. They are not equivalent. For example, the function $f$ defined as $f(a,c)=(1,1)$ if $a=c$, otherwise $f(a,c)=(0,0)$, is in (A * C) -> (B * D) (assuming $0,1 \in $ B,D), but has no corresponding element in (A -> B) * (C -> D). As you say, the number of elements in those two sets is different, so they cannot be isomorphic.