Re: [Haskell-cafe] type and data constructors in CT

On Sun, Feb 1, 2009 at 12:36 PM, Gregg Reynolds wrote:

On Sat, Jan 31, 2009 at 3:14 PM, David Menendez wrote:

...

There's a paper about defining catamorphisms for GADTs and nested recursive types that models type constructors that way.

If you recall a title or author I'll google it.

I believe it was "Foundations for Structural Programming with GADTs". http://crab.rutgers.edu/~pjohann/popl08.pdf

...

...

So this gives us two functors, but they operate on different things, and I don't see how to get from one to the other in CT terms. Or rather, they're obviously related, but I don't see how to express that relation formally.

Again, what sort of relationship are you thinking of? Data

Ok, good question. I guess the problem I'm having is one of abstraction management. CT prefers to disregard the "contents" of its objects, imposing a kind of blood-brain barrier between the object and its internal structure. Typical definitions of functor, for example, make no reference to the "elements" of an object; a functor is just a pair of morphisms, one taking objects to objects, the other morphisms to morphisms. This leaves the naive reader (i.e. me) to wonder how it is that the internal stuff is related to the functor stuff.

Right. The reason the definition of functor doesn't say anything about the "internal stuff" is that there are plenty of categories where there *is* no internal stuff. So for categories like Set or Mon, where the objects to have elements, category theory uses morphisms to describe their internal structure. For example, a set is an object in Set, and its elements are morphisms from the singleton set. So if I have some operation that creates a monoid from a set, and transforms set functions into monoid homomorphisms in a way that respects identity functions and composition, then I have a functor from Set to Mon. (For example, the free monoid that Wren mentioned.) Whatever internal stuff is going on will be reflected in the morphism part of the functor, because otherwise the functor can't map the morphisms correctly.

For example: is it true that the object component of a functor necessarily "has" a bundle of specific functions relating the internal "elements" of the objects? If so, is the object component merely an abstraction of the bundle? Or is it ontologically a different thing?

Let me try to give an illustrative example. Consider a category A with a single object and a bunch of morphisms from that object to itself. Now, the object itself isn't interesting, which is why I didn't give it a name. It's not any kind of set, and the morphisms aren't functions: composition just combines them in some unspecified manner. Because A is a category, we know that there's an identity morphism id, such that f . id = f = id . f, and we know that f . (g . h) = (f . g) . h. In other words, the morphisms in a single-object category form a monoid. What's more, since we don't care about what the morphisms are, we can take any monoid and create a single-object category. For example, we could define a category Plus where the morphisms are natural numbers, the identity morphism is 0, and morphism composition is addition. Now let's say we have to single-object categories, A and B, and a functor F : A -> B. What do we know about F? We know that F maps the object in A to the object in B, and it maps the identity morphism in A to the identity morphism in B, and that for any morphisms f and g in A, F(f) . F(g) = F(f . g). In other words, F is a monoid homomorphism (that is, a mapping from one monoid to another that respects the identity and the monoid operation). We can define other functors, too. For example, a functor P : Plus -> Set. We'll map the object in Plus to N (the set of natural numbers), and every morphism n in Plus to a function (\x -> n + x) : N -> N. You can prove for yourself that P(0) gives the identity morphism for N, and that P(m + n) = P(m) . P(n). So P is a functor whose object component doesn't have a bundle of specific functions relating the internal elements of the objects. All the interesting stuff in P takes place in the morphism map. Does that help at all? (A side note: As I said, for any monoid X, we can create a category C(X), and it's obvious that for any monoid homomorphism f : X -> Y, we can create a functor C(f) : C(X) -> C(Y). It turns out that for any monoids X, Y, and Z and homomorphisms f : Y -> Z and g : X -> Y, C(f) . C(g) = C(f . g). So C is a functor from the category of monads to the category of categories.) -- Dave Menendez http://www.eyrie.org/~zednenem/