On Sat, Jan 31, 2009 at 3:14 PM, David Menendez
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