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

StackOverflow https://stackoverflow.com/questions/12571161

Domanda

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:

enter image description here

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:

enter image description here

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:

enter image description here

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?

È stato utile?

Soluzione

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(0) 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(1), 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→CB, which allows the object CB 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(2).

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.

Altri suggerimenti

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.

Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a StackOverflow
scroll top