Presented by Arnaud Bailly and Christophe Thibaut

Abstract:

This session is about “climbing the abstraction ladder” using category theory, or more precisely trying to do so. The presenters are fascinated by category theory and want to explore with participants how this thing (which has sometimes been dubbed “abstract nonsense”) could be put to use in software design. The basic premise is that, while BDUF is bad, we need generally to put more thinking in designing our software and more specifically we need tools to find and exposes abstraction earlier in the process. The categorical framework might be such a tool… or not.

A Category is a mathematical object from abstract algebra (eg. akin to things like groups or monoids) which can be viewed as a directed graph. It imposes a structure with objects and relations between them. One classical example of a category, called Set is the category of all sets together with the total functions between them.

In computer science, Cat. theory is used in various fields relating to semantics of programming languages, type theory, compilation… Another classical category is Haskell’s type system (not quite true, I think, but close to it) or more generally ML-languages type system. And any directed (possibly labelled) graph may also be viewed as a category.

The main theme of Category Theory is composition: How one can compose things together and what structures arise from this composition.

Session is not meant to be a master’s degree course on Category Theory, but rather a collective exploration of its abstraction power and how it could be harnessed to develop better, thinner, faster and clearer software.

Format and length:

Tentative agenda:

• Basic introduction to category theory: What it is? Where it comes from? What it is used for?
• Core concepts + exercises/exploration on OO models: Objects, arrows, composition, basic objects…
• Higher-level concepts + exercises on differents models (eg. types, relational/OO, OO/XML, X-model): Functors, natural transformations

Objective(s) of the session:

• Remove a veil of magic and mysticism that might cover such heavy words as category theory, functors, morphisms or natural transformation that might appear here and then in CS and PL litterature,
• Explore within categorical framework the power of abstracting from the details of objects to explore the structure of their relationship: Given a specific collection of objects or classes, or a specific piece of code, use categorical constructions to capture some abstract property of the structure, or to identify what prevents this abstraction process to take place,
• Try to assess the usefulness of Cat theory as a tool for designing software and systems: Can we use Cat theory concepts as a sieve to assess useful and important properties about our software?

Benefits for participants and presenter(s):

• A new tool in their toolbox