[Haskell-cafe] type and data constructors in CT

[David Menendez]

On Sun, Feb 1, 2009 at 12:36 PM, Gregg Reynolds <dev at mobileink.com> wrote:
> On Sat, Jan 31, 2009 at 3:14 PM, David Menendez <dave at zednenem.com> 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 <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>