[Haskell-cafe] type and data constructors in CT

[Derek Elkins]

On Sat, 2009-01-31 at 11:00 -0600, 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.

The typical (albeit incomplete) view is that data constructors are the
(components of the) initial algebra of the functor corresponding to the
signature of a given algebraic data type.  This is discussed in quite a
few places online. 

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

What are "elements" of a type?  How are you "construing a type as a
category"?  One answer is that you are viewing types as sets.  Ignoring
the problems with that identification, a set can be viewed as a discrete
category and functors between discrete categories are just functions.
This is like going around three sides of a square; you don't gain
anything over just saying "types are sets, and functions are set
functions."

Note that there is nothing special about data constructors here.  Every
function between types is such a functor.

Most articles that apply CT to Haskell take one of two approaches.  They
either talk about a category of Haskell types and functions with no
explanation of what those "actually" are, i.e. the understanding that it
behaves like (idealized) Haskell, or they refer to some existing
approach to (idealized) semantics, e.g. sets or domains.  In either
case, the meaning of the objects and arrows is effectively taken for
granted.

An approach along the lines you are suggesting would be useful for a
categorical semantics of Haskell, but it would just be one possible
semantics among many.  For most of the aforementioned articles, the only
value of such a thing would be to be able to formally prove that the
constructions talked about exist (except that they usually don't for
technical reasons.)  Usually in those articles, the readers are assumed
to know Haskell and to not know much about category theory, so trying to
explain types and functions to them categorically is unnecessary and
obfuscatory.  It would make sense if you were going the other way,
explaining Haskell to categorists.

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

One way to do this would be to use indexed categories or more generally
two categories.