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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
