[Haskell-cafe] type and data constructors in CT

[Gregg Reynolds]

On Sat, Jan 31, 2009 at 5:11 PM, Derek Elkins <derek.a.elkins at gmail.com> 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.
>
> 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

That's a good question.  I've been hoping that viewing types as sets
is good enough but that doesn't seem to be the case.

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

You can say that again.
>
> 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.

Actually, what I have in mind using the concepts and terminology of CT
to explain Haskell to ordinary programmers.  The idea is not
necessarily to prove stuff, but to build the intuitions needed to
think about computing at a higher level of abstraction before
proceeding to Haskell.  I suspect this might be the quicker road to
Haskell mastery; even if not it's a fun writing project.  Call me
nutty, but I think the basic concepts of CT - category, functor,
natural transformation, monad - are actually pretty simple, even
though it took much gnashing of teeth for me to acquire a basic
intuition.  You don't have to be a mathematician to see the basic
structural ideas and get some idea of their usefulness, /if/ you have
appropriate pedagogical material.  Alas, I've found that clear, simple
explanations are scattered across lots of different documents.

Thanks for your help; I can see I've got a few more things to work on
(like "type").

-gregg