Are functions of arity-n really just an n-category due to currying? Can they be made into a 1-category?

Question

This question has a longish prelude before I can actually ask it :)

Let's say type A and B represent categories, then the function

f :: B -> A

is a morphism between the two categories. We can create a new category with A and B as objects and f as the arrow like this:

Now, let's introduce a new category C and function g:

g :: C -> B -> A

I would like to be able to add C and g to my category above, but am unsure how to do it. Intuitively, I want something that looks like this:

But I've never seen anything like that in a category diagram before. To make this kosher, I could introduce a dummy arrow g' and construct a 2-category like this:

But that seems like an obtuse picture. (We could, of course, use the picture I drew above as shorthand for the proper one.) Also, it's not exactly clear anymore what g and g' even are. g is no longer a function that takes as input a category C and returns a morphism :: B -> A. Instead,

g' :: (C -> C)

g :: (C -> C) -> (B -> A)

If we pass g the identity, then everything will work fine. But if we pass it some other function, then who knows what could happen?

So my question is: Is an n-arrow within an n-category really the way we should think about functions with arity n? Or is there some easier way to represent this function down into a standard category that I missed?

Hittel

Here's my understanding, but IANACT. Normally, in this context, you solve this by working inside a cartesian closed category: one which has both finite products and exponentials. An exponential object A^B is one which is in a precise sense equivalent to the arrow B → A; in particular, there exists an evaluation map apply : A^B × B → A with the requisite universal properties. Thus, g :: C -> B -> A corresponds to g : C → A^B. ('^' denotes superscript.) – Shopwindow

@AntalS-Z: Closed categories are not necessarily cartesian--there's more to life than typed lambda calculus. :] Also, the object A^B is equivalent to the collection of arrows B -> A; an individual arrow corresponds to an "element" of the object. – Misfit

@C.A.McCann: Thanks for the corrections! Like I said, I don't actually know what I'm talking about :-) – Shopwindow

Answer 1

Talking about "morphisms between categories" here sounds like a possible category error (ha, ha). In Haskell we most often talk about an alleged category Hask, which is some inconsistently idealized⁽⁰⁾ version of the category whose objects are types of kind * and morphisms are functions. It's unclear what "functions" between categories would be here, if they're not morphisms of Hask.

On the other hand, in a more general setting you can certainly define a category whose objects are other categories⁽¹⁾, with whatever morphisms you want such that the necessary properties are satisfied. The usual example of this is Cat, the category of small categories whose morphisms are functors.

That said, in either case the answer to your question is essentially the same. To talk about the collection of morphisms between two objects as if that collection was itself an object--i.e., as source or destination of other morphisms--you need an object to fill that role and some way to indirectly talk about morphisms so that you can translate back and forth.

One way to do this, if we already have a way to talk about pairs of objects as a single object (usually called a "product" of some sort), is to define an equivalence between the collection of morphisms A⊗B→C and the collection of morphisms A→C^B, which allows the object C^B to stand in for the collection of morphisms B→C.

If the "pairs of objects" in question are in fact a categorical product, we have a cartesian closed category, which both Hask and Cat are. In Haskell, the above equivalence are the functions curry and uncurry⁽²⁾.

That's not the only way to talk about morphisms-as-objects, of course. The general concept is simply called a "closed category". But if you're thinking in terms of higher-order functions and functional programming, a cartesian closed category is probably what you have in mind.

---

(0) This usually involves things like pretending ⊥ doesn't exist (so that all functions are total) and treating functions that produce the same output as identical (e.g., ignoring differences in performance).

(1) But don't try to talk about a category whose objects are all categories, or else Bertrand Russell's gonna give you the business.

(2) Named after, of course, the logician Haskell Curry.

Misfit

This seems isomorphic to my n-category formulation. Is it true that any n-category can be equivalently represented by a 1-category with a similar construction? – Hittel

@MikeIzbicki: I'm not entirely clear on what your formulation means, to be honest. As far as I understand it, 2-morphisms are only defined between 1-morphisms whose source and target are the same. Going between two unrelated morphisms seems like something else entirely. – Misfit

@C.A.McCann: as an aside, is it true that the category of all categories leads to Russell's paradox? After all, there's not an axiom of separation for categories. – Discoid

@BenMillwood: Well, it depends on what your basic definitions are. If you define categories in terms of classes of objects/morphisms and ignore size issues, of course you get the same trouble. If you account for size in a set-theoretic manner, "the category of all small categories" is analogous to "the class of all sets". If you throw out set theory in favor of CT-based foundations things may look different, with perhaps a more fine-grained notion of "size". But, if you expect to build set theory on top of category theory you clearly can't escape the issue entirely. – Misfit

Do I understand right that there is no analogy to currying in category theory (applicable to Hask)? – Glazing

@egdmitry: I'm not sure where you're getting that. The definition of a cartesian closed category is essentially "a category that allows currying". That's almost too direct to even call it a mere "analogy". – Misfit

Sorry, I was confused with something. Now I got it. Thanks! – Glazing

Answer 2

I'm fairly unschooled in category theory, but:

In Haskell programming we often (pretend that we) work with the category Hask, whose objects are Haskell types and morphisms are Haskell functions.

Applying that understanding to your example, I see that B and A are objects, and f is a morphism between them.

g is however not a morphism between C and f, so there should be no attempt to draw g as an arrow between C and the f arrow.

If we apply the right-associativity of the -> type constructor, we get g :: C -> (B -> A). B -> A itself is a Haskell type, and so should be an object of Hask in its own right. f is however not that object; it is one particular value in the type B -> A, but the B -> A object would be the type itself.

This also makes sense thinking purely in Haskell terms. Just because g applied to a value of type C gives us some function of type B -> A, that doesn't mean g's return value has anything to do with f, which is some other function of type B -> A.

So that gives us f as a morphism drawn between the object B and the object A, and g as a morphism drawn between the object C and the object B -> A.

Here's where my category theory knowledge breaks down. It seems obvious that there should be some sort of relationship between f and the object B -> A, as in Haskell f is a value in the type B -> A. I don't know what that relationship is in category theory terms.

C. A. McCann's answer makes it sound like you need to handle that by some "extra" relationships that aren't modelled directly by the category. So as far as the category is concerned, the object B -> A might as well be called D; it has no relationship to anything else except as given by the morphisms connecting it to other objects. It's only in combination with other information from "outside" the category that we can identify the connection between A, B, f, and D (really B -> A). But I may be misunderstanding that description.

Derrek

I think (but am not sure) that you're wrong about g not being a morphism from C -> f. f in this case is not the type B -> A, but a specific instance of that type. For example, I could have three different morphisms f, f', and f'' each :: B -> A. We would draw those as three separate arrows in the diagram. Thus it would make sense to draw the arrow g from C to f but not to f' or f''. – Hittel

@MikeIzbicki But if g :: C -> B -> A, then the function resulting from applying g to a value from C is of type B -> A, but it will (in general) be different for each possible value from C, and it is unlikely that any of the functions generated by g will be related to f. That's why I say g should not correspond to an arrow drawn to f. – Derrek

Keep in mind that "no relationship to anything else except as given by the morphisms" describes the CT notion of an object in general, so it's to be expected that describing equivalences between morphisms is used to define exponential objects. The categorical product is defined similarly, by equivalences involving morphisms that correspond to fst, snd, and (&&&) in Haskell. – Misfit

Approaching things from the other side, if you take any specific category of types/sets/&c. with functions as morphisms and an existing notion of functions-as-values, it's very often the case that whatever is analogous to a cartesian product (in Haskell, (,)) is the categorical product and that functions-as-values are exponential objects. The definition in terms of equivalent morphisms captures the essential behavior these examples share. – Misfit