[Haskell-cafe] type and data constructors in CT

[wren ng thornton]

Gregg Reynolds wrote:
> Hi,
> 
> I think I've finally figured out what a monad is, but there's one
> thing I  haven't seen addressed in category theory stuff I've found
> online.  That is the relation between type constructors and data
> constructors.
> 
> As I understand it, a type constructor Tcon a is basically the object
> component of a functor T that maps one Haskell type to another.
> Haskell types are construed as the objects of category "HaskellType".
> I think that's a pretty straightforward interpretation of the CT
> definition of functor.

Yes. Of course, Tcon is only a functor if it takes a single type 
argument. It's a bi-functor if it takes two, etc.

[This category is typically called "Hask". However there are some 
technicalities about really constructing a category with Haskell 
functions as morphisms, due to strictness issues and the like.]


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

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.

As Ben Moseley said, oftentimes when you have this pattern (the image of 
an endofunctor on a category forming a subcategory) it's the result of a 
natural transformation. The morphisms are the unit/eta morphisms. To 
make the details work out for types with many constructors, you may need 
to bundle the Dcon morphisms together into a coproduct morphism in order 
to get the unit. You get a similar pattern with parametric polymorphic 
functions for the same reasons (see how the forall was dealt with 
above). Whether a type constructor or polymorphic function is a natural 
transformation or not depends on the type as well as how/whether it has 
an fmap etc.


[To be pedantic, we could call data constructors functors (instead of 
morphisms) if we set up the types (originally objects in Hask) as 
individual categories themselves (with values as their objects)[1]. It's 
just a question of resolution and what we're focusing on at the moment. 
These sorts of towers of categories are actually not that uncommon with 
programming languages. If we wanted to go upwards in resolution instead, 
we could talk about different Hask categories for different programs as 
our objects, with semantics-preserving transformations as the morphisms, 
for example.

[1] Any type ---being a set--- can be described as a category trivially 
so long as we make it a discrete category (the only morphisms are id). 
However, this isn't very interesting since it says nothing about the 
structure actually inherent in the type (e.g. for a recursive type of 
trees, how bigger trees can be made from smaller ones; or for other 
types the monoid,semiring,ring,field,group,etc structure).]

-- 
Live well,
~wren