0
$\begingroup$

First of all, I have absolutely no knowledge in computer science. I am reading this in context with category theory, in particular the general tensor-hom adjunction.

Suppose we're living in $\mathsf {Set}$. This $n$lab entry on currying suggests denoting by $\vdash$ the external hom and then to generalize currying $$f:X\times Y \vdash Z$$ to produce $$\hat f:X \vdash Y \rightarrow Z$$ without need for parenthesis.

Questions:

  1. Unless I am misunderstanding, $A \vdash B= [A,B]$, so going from left to right, $X\times Y \vdash Z=[X\times Y,Z]$ which is a set, so we have have $$f:\text{some set}$$instead of a domain and range for $f$. What does this notation mean?
  2. What exactly does "without need for parenthesis" mean? Certainly $[X\times Y,Z]\neq X\times[Y,Z]$
  3. How does this generalize currying?
  4. Changing the scheme to $$\frac{f:X\times Y\rightarrow Z}{\hat f:X\rightarrow Y\vdash Z}$$ seems to make more sense and even suggests an adjunction $(-\times Y) \dashv (Y\Rightarrow-)$ (which I think is exactly the tensor-hom adjunction since $\mathsf{Set}$ is cartesian closed). Why isn't this the right formulation?
$\endgroup$
1
  • $\begingroup$ In the nLab article, $A \to B$ is used for what a categorician usually writes $B^A$ or $A \Rightarrow B$. And $f \colon A \vdash B$ is used to say $f$ is a morphism from $A$ to $B$. In your questions, you seem to assume the other way around. $\endgroup$
    – Pece
    Dec 24 '14 at 14:51
1
$\begingroup$

I am going to come at this from a purely computer-science perspective.

Regarding your fourth question (i.e., why not write $\hat f\colon X\rightarrow Y\vdash Z$), when I studied type theory we did not distinguish between internal hom and external hom. We used one symbol where $n$Lab uses two, so we would have written $$\frac{f\colon X\times Y\rightarrow Z}{\hat f\colon X\rightarrow Y\rightarrow Z}.$$

At that time, the computer-science type theorists I knew had just started talking to category theorists, so possibly they have refined their notation since then. But my sense from $n$Lab is that the choice there to write $\hat f\colon X\vdash Y\rightarrow Z$ rather than $\hat f\colon X\rightarrow Y\vdash Z$ was somewhat arbitrary. That is, when $n$Lab says computer science uses $\rightarrow$ for the internal hom, one could just as accurately say that computer science uses $\rightarrow$ for the external hom, which would lead to using a different symbol for the internal hom, possibly even writing the rule for currying just as you suggest.

But the first arrow was always implicitly distinguished from any other arrows in a curried function, because (using type-theoretic language) the type on the left of that arrow was the domain of $\hat f$ and the type on the right was the range.

The phrase "without need for parenthesis" refers to what happens when the uncurried function takes more than two variables. In particular, using the type-theoretic notation I'm familiar with, $$ f \colon X_1 \times X_2 \times \cdots \times X_{n-1} \times X_n \rightarrow Z $$ is the same thing as $$ f \colon (X_1 \times X_2 \times \cdots \times X_{n-1}) \times X_n \rightarrow Z $$ and so one can set $X = X_1 \times X_2 \times \cdots \times X_{n-1}$ and $Y = X_n,$ apply the rule for currying $f\colon X\times Y\rightarrow Z,$ and write $$\hat f\colon X_1\times X_2\times\cdots\times X_{n-1}\rightarrow (X_n\rightarrow Z).$$ By repeated application of this rule you get to $$\hat{\dot{\dot{\dot{\hat f}}}}\colon X_1\rightarrow(X_2\rightarrow\cdots\rightarrow (X_n\rightarrow Z)\cdots)$$ which can be written simply as $$\hat{\dot{\dot{\dot{\hat f}}}}\colon X_1\rightarrow\cdots\rightarrow X_n\rightarrow Z.$$

I think this is what $n$Lab meant by a generalization of currying, although I would regard it merely as repeated application of currying. Possibly the $n$Lab statement was meant to be read differently than I did.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy