1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Your question is hard to read because of formatting. Note that you can use LaTeX here to typeset mathematics in a more readable way. See here for a short introduction. $\endgroup$
    – Nathaniel
    Commented Jan 21, 2023 at 15:21
  • 1
    $\begingroup$ Can you cite one source that claims (A -> B) * (C -> D) = (A * C) -> (B * D)? Is there any context in that source or any explanation or justification for this claim? $\endgroup$
    – D.W.
    Commented Jan 22, 2023 at 3:08

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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