Home » forums » LtU Forum

Category theory in design

I have seen mentioned in this site that category theory is useful in clarifying the design process. I am wondering if the categorical approach would be any different from a purely functional approach. My reasoning is that in category theory, objects (states and data) are not important, if not almost entirely dismissable. What is of importance to the categorists is the relationships between objects, the functions, the way the structures work. It seems to beg the question, is category theory an abstraction of functional programming (not in an intuitive manner, but in the strict sense) and is there anythings that would be explanable in category theory that would not be in a functional language and the converse?

By jdgallag at 2008-05-23 23:39 | LtU Forum | previous forum topic | next forum topic | other blogs | 8242 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Quote

What we are probably seeking is a "purer" view of functions: a theory of functions in themselves, not a theory of functions derived from sets. What, then, is a pure theory of functions? Answer: category theory.

                                                                                Dana S. Scott, Relating theories of the λ-calculus

By Paul Snively at Sat, 2008-05-24 17:29 | login or register to post comments

I agree. Then would you

I agree. Then would you agree, that it would be worthwhile to come up with a categorically oriented programming language?

My original question remains: how would a categorically oriented programming language differ from a functional one?

My opinion is that in a categorically oriented language, it may be fine to think of functors, transformations, and maybe even use parts of categorical logic in a first class manner. I just cannot think of a reason that would be different from higher order functions.

By jdgallag at Sat, 2008-05-24 20:00 | login or register to post comments

This previous post will be

This previous post will be of interest. Particularly the thesis mentioned.

By naasking at Mon, 2008-05-26 17:36 | login or register to post comments

José Luiz Fiadeiro's book

José Luiz Fiadeiro's book Categories for Software Engineering applies categorical concepts to computing in a very different way from the usual type-theoretic, functional programming point of view where morphisms in Cartesian closed categories represent computations. The basic idea (although I can't claim to have done anything other than skim the book) seems to be to use categories to describe aspects of software components and component engineering, e.g. modularity, refinement relationships, composition, features, etc.

To the best of my limited knowledge these approaches haven't yet precipitated into any actual programming languages, but perhaps they point to at least one sense in which a "categorically-oriented programming language" might differ from a language like Haskell.

By Roly Perera at Sun, 2008-05-25 14:15 | login or register to post comments

Could you name some of the

Could you name some of the books, online readings where the usual type-theoretic point is discussed, please?

Zsolt

By Zsolt Szalai at Sun, 2008-05-25 18:54 | login or register to post comments

Previously on LtU

A discussion on introductory category theory for CS folk.

By James Iry at Sun, 2008-05-25 20:51 | login or register to post comments

Goguen school

Judging from his worshop slides (for "Categorical Structures for System Modelling", available as ZIPped pdf & quicktime from his homepage), his general approach follows that of Joseph Goguen's approach to algebraic datatypes, which uses various sorts of reasoning with limit and colimit constructions over cartesian categories, which are usually not closed, and which provide good algebraic structures for modelling equational logics. There are quite a lot of programming languages based on this; probably the first places to look at are Goguen's OBJ3 language, based on order-sorted cartesian categories, and Maude, which is based on rewriting logic.

Joseph Goguen put up a page on the OBJ family of languages.

Postscript: I see that Fiadeiro's CommUnity language, which is used in his book, has its operational semantics based on rewriting logic.

By Charles Stewart at Tue, 2008-05-27 08:57 | login or register to post comments

System specification

The best example of category theory being used for something in CS design that isn't immediately obviously reducible to something based in a functional language would be specifying systems, particularly system configuration. Mostly here I'm thinking in terms of things like presheaves as configured specifications, presheaf models for concurrency, coalgebraic class specification, and coalgebra in general as a theory of systems.

Now all of those are not strictly pure category theory, but are ultimately best understood from a categorical framework. Nor am I sure that they are not expressible in a functional language -- it just doesn't seem immediately obvious to me how to do so (or even why you would want to). A final proviso: I am a mathematician, not a computer scientist, so my understanding of the CS aspects of this is somewhat limited.

By Leland McInnes at Sun, 2008-05-25 21:54 | login or register to post comments

yes

Pure category theory might not even be practical in the areas above, yet this is the kind of thing I was talking about. Those articles show ways that using category theory can help design, even to the point of making system specification and design mechanical and provable. Perhaps it would be worthwhile to utilize these ideas in a generic sense and create CASE tools that explicitly make use of the patterns found in category theory.

I believe there is a point here outside of design that I am addressing though. Many, if not most of the ideas of categories where examining a single category can be expressed using higher order functions, such as map, and beyond that relationships of functors between more than one category can be expressed with higher-order functions as well.

However, it is not clear that (the main purpose of category theory) natural transformations and adjoints would have an easy or intuitive specification in a primitive recursion or second order recursion. I think that designing a language that can handle natural transformations and adjoints in a first class way, so that the programmer could just use them, has the potential to make algorithm specification a bit easier. Instead of utilizing two functors say F and G and a two functors that map F onto G and G onto F; one could just call { nTrans args } and not worry about it. I am just not sure how much this would be useful outside of technical math work and/or theorem proving, or if there is a subtlety about how to simply do it in a functional language that I have missed.

By jdgallag at Mon, 2008-05-26 19:26 | login or register to post comments

See above

If you haven't yet, you should definitely look at the thread linked by naasking earlier. And you should definitely look at Tatsuya Hagino's thesis.

By Matt Hellige at Tue, 2008-05-27 16:03 | login or register to post comments

For an alternative view

For an alternative view of the role of category theory in design take a look at the work of Doug Smith and his colleagues. E.g. ftp://ftp.kestrel.edu/pub/papers/pavlovic/unuiist-kestrel.ps. A rather shallow summary of the idea, as i understand it, is software design by refinement. Given a pre-existing taxonomy of refinements (morphisms) in a library, if a match between your problem spec and a library component can be found (another morphism), then the required refinement of your spec is the pushout of the two morphisms. Once the particular library refinement has been identified, the pushout can be mechanically computed.

By snedunuri at Thu, 2008-05-29 15:49 | login or register to post comments