[Haskell-cafe] type and data constructors in CT

[Gregg Reynolds]

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.

>> 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.

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?
Hence my question about constructors in Haskell: the type constructor
operates on the opaque object (type); the data constructor operates on
the values (type as transparent object?).  A type and its values seem
to be different kinds of things, so there must be some way to
explicitly account for their relationship.  I figure either I'm
missing something about functors, or I need a more sophisticated
understanding of type-as-category.

Anyway, thanks to you and the other responders I have enough to go
away and figure it out (I hope).

Thanks,

gregg