Isomorphism is not about currying. When I mentioned isomorphism, I was referring to the interchangeability in general, and the currying relationship is just an

Isomorphism is not about currying. When I mentioned isomorphism, I was referring to the interchangeability in general, and the currying relationship is just an example of an isomorphism. In category theory notation: Hom(A * B, C) ~ Hom(A, C ^ B) This is one of the laws of a Cartesian closed category. The simply typed lambda calculus with products is the internal language of a Cartesian-closed category.