Hello,
what is the relation between Category Theory and (Computer) Program Construction ? Don't hesitate to substitute "(Computer) Program Construction" by another, maybe weaker expression, if you feel to.
Thanks,
Claus
Dear Claus, Here's one view. An important technique in program construction is modularization in such a way that the concrete data structures and program code are concealed. The programmer who uses that module is expected to work by its API (Applications Program Interface), not by knowledge of its implementing code - that allows the module implementation to be corrected or updated without affecting the callers. To do that relies on knowledge of possible external relationships between the module and the application programs, independent of knowledge of its internal code, and there are various techniques for doing this. Some are more precise than others. Examples are the informal descriptions of Java APIs and the requires/ensures specifications in Eiffel. I haven't got to category theory yet, but actually category theory is doing something similar. Category structure conceals the internal structure of objects and instead formalizes a notion of "external relationship between objects" (the morphisms). It then uses the idea of universal property to characterize the external interface of objects (e.g. product, coproduct, exponential characterized in terms of morphisms to and from other objects). In any given category you prove that such constructions exist by "implementing" them in terms of the definition of object for that particular category, but once that is done it is usually best to handle them through the universal properties. That's just woolly analogy so far. I'm certainly not saying that the Java API uses a category. But where it has been put rather sharply into action is in the semantics of programming languages. The syntax of a language is its internal structure. What is important to the programmer is the meaning of each syntactic construct, and that needs to be explained in some external way. Category theory has provided a way of doing this for a wide variety of languages so that - e.g. - record types might be explained as products, sequencing as composition of morphisms. A categorical semantics helps to explain program constructs by what you can do with them (external) rather than how you write them down (internal), and has effectively provided a means of comparison of syntactically different languages. To summarize this particular view: category theory is a mathematical theory of modularization. Steve Vickers.