[Haskell-cafe] type and data constructors in CT

[David Menendez]

On Sat, Jan 31, 2009 at 12:00 PM, Gregg Reynolds <dev at mobileink.com> wrote:
> 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.

What sort of relationship are you expecting?

Type constructors and data constructors are injective functions, and
the language takes advantage of that in various ways. (E.g., type
constructors are allowed, but not general type functions. Data
constructors support pattern-matching.) Aside from playing analogous
roles and having similar names, I'm not sure there is a deeper
relationship.

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

If Hask is the category of Haskell types and functions, and |Hask| is
the discrete category of Haskell types and (only) identity functions,
then you can model a type constructor of kind * -> * as a functor from
|Hask| to Hask.

There's a paper about defining catamorphisms for GADTs and nested
recursive types that models type constructors that way.

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

Sure. If nothing else, any set can be made into a discrete category,
and functors from discrete categories are basically functions.

> 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
constructors always construct values of types of kind *, and people
discussing type constructors are usually talking about kinds at least
as complex as * -> *.

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>