On Sat, Jan 31, 2009 at 5:11 PM, Derek Elkins
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