[Haskell-cafe] type and data constructors in CT

[Gregg Reynolds]

On Sat, Jan 31, 2009 at 4:26 PM, wren ng thornton <wren at freegeek.org> wrote:

>> But a data constructor Dcon a is an /element/ mapping taking elements
>> (values) of one type to elements of another type.  So it too can be
>> construed as a functor, if each type itself is construed as a
>> category.
>
> Actually no, it's not a functor. It's a (collection of) morphism(s). Let's
> again assume a single-argument Dcon for simplicity. The Haskell type |Dcon
> :: forall a. a -> Tcon a| is represented by a collection of morphisms
> |Dcon_{X} : X -> Tcon X| for each X in Ob(Hask).

Ok, I see I elided that step.  So my question is about the relation
between the individual (specialized) Dcon and the associated Tcon.
I.e. Dcon 3 is a value of type Tcon Int, inferred by the type system.
So it looks to me like the relation between the Tcon functor and the
Dcon functions is basically ad hoc.  You use Tcon to construct new
types; you can define any function you wish to map values into that
type.  The Haskell data notation is just a syntactic convenience for
doing both at once, but the functor has no necessary relation to the
functions.  (Flailing wildly...)
>
> It's important to remember that Tcon is the object half of an *endo*functor
> |Tcon : Hask -> Hask| and not just any functor. We can view the object half
> of an endofunctor as a collection of morphisms on a category; not
> necessarily real morphisms that exist within that category, but more like an
> overlay on a graph. In some cases, this overlay forms a subcategory (that
> is, they are all indeed morphisms in the original category). And this is
> what we have with data constructors: they are (pieces of) the image of the
> endofunctor from within the category itself.

(unknotting arms...) Uh, er, hmm. I'm still having abstraction
vertigo, since we have (I think) data constructors qua generic
thingees that work at the level of the category, and the same,
specialized to a type, qua functions that operate on the internals of
the categorical objects.  It's the moving back and forth from type and
value that escapes me, and I'm not sure I'm even describing the issue
properly.   I shall go away and thing about this and then write the
answer down.

Thanks much, you've given me a lot to think about.

-gregg