How are types defined in category theory

Category theory and types

  • Lecture, Dr. E. Richter, Wed. 10: 00-12: 00, changing rooms, see below!
  • Exercise, T. Richter, Fri. 10: 00-12: 00, changing rooms, see below!

The event is incorrectly identified in PULS as "CATEGORY THEORY AND LOGIC". A correction is in progress.

Lecture and exercise take place in rooms that change on a weekly basis. Here is the exact room plan:

V 04/15-
U 04/17S27
V 04/22S12U 04/24S14
V 04/29S18U 01.05.S12
V 06.05.S12U
V 13.05.S12U 15.05.was cancelled
V 05/20S21U 22.05.S13
V 27.05.S12U 05/29S15
V 03.06.S13U 05.06.S22
V 10.06.S12U
V 17.06.S13U June 19.1.02
V 24.06.S12U 26.06.S14
V 01.07.S12U 03.07.S18
V 08.07.S12U 07/10.S19
V 07/15S12U 07/17.S19
V 07/22S12U 07/22S19

It has been almost 50 years since the categories were first mentioned as semantics for the lambda calculus. Nowadays it is difficult to find a text on the theory of programming languages ​​that does not mention categories. The reason for this is the fact that both category theory and the theory of programming languages ​​are essentially "function theories".

The concept of a morphism - that is the categorical correspondence of functions - is a generous generalization of the set-theoretical concept of functions and forms a kind of universal tool with the help of which various aspects of the theory of programming languages ​​such as type theory, generic programming and optimization can be found in a uniform Can describe language.

However, the influence of category theory has also become more and more important in other areas of computer science in recent years. One often finds categorical approaches e.g. in software development, AI, automaton theory and other theoretical areas. Not only are the results of categorical constructions used directly, but category theory is also used as a mathematical language.

One of the core ideas of category theory, to always consider abstract structures together with the associated (i.e. structure-preserving) relationships, has proven to be extremely fruitful; it facilitates the creation of a mathematical taxonomy, often a primary goal of scientific analysis. Often there are multiple formalisms and structures for something that is basically the same concept. The categorical language is simplified by abstraction and it often turns out that the concept sought is a categorical construction and the various formalisms are their realizations in different categories.

Our lecture has a twofold purpose. On the one hand, it should explain the connection between category theory and type theory, on the other hand, it should also familiarize you with the categorical way of thinking as a tool.

The lecture is divided into 4 chapters. The introductory chapter deals with orders, associations and the basics of the semantics of functional programming languages. In this way, on the one hand, concrete mathematical structures are introduced, on the other hand, the thought schemes common in category theory are implemented in concrete terms, so to speak. We will always refer to the terms discussed in this chapter as "running examples".

In the second chapter we define the basic terms such as category, functor, natural transformation, adjunction and monad. We introduce various categorical constructions and prove some basic relationships. Many books on category theory use examples and motivations from algebra and geometry, which of course only help readers who are familiar with the relevant areas of mathematics. Instead, to illustrate the concepts, we will refer to the terms introduced in Chapter 1 as well as to elementary mathematical structures common to each
Computer science students are familiar with focus. We will also look at some techniques of functional programming and results of the computability theory as the realization of certain categorical constructions. For example, we will see that the s-n-m theorem is only a concrete formulation of the existence of the exponential in the category of partially computable functions.

The third chapter begins by showing how the definition of a category is linked to the derivation of judgments (i.e., terms-in-context) of an algebraic type theory, which gives us a first look at the close relationship between category theory and type theory.

Finally, in Chapter 4 we introduce functional type theory based on the singly typed lambda calculus. This is a formal syntactic language and can be viewed as a very simple programming language. Finally, we characterize categories that are suitable as semantics for programming languages ​​with extended type constructs, such as dependent data types and polymorphic functions.

Category theory is a very abstract language. In order to acquire their terms and to grasp their scope, it is necessary that the learner
worked through as many examples as possible. Therefore, the lecture is supplemented by a tutorial. During the first part, the tasks mainly include the execution of categorical constructions as so-called diagram hunts on paper. In the further course this part is supplemented by practical exercises with a formal system, i.e. programming of concepts in a functional language.


The guiding text is

  • Crole: "Categories for Types", Cambridge Mathematical Textbooks, 1993

Further IT-friendly introductions are

  • Awodey: "Category Theory", Clarendon Press, Oxford 2006
  • Adámek, Herrlich, Strecker: "Abstract and Concrete Categories - The Joy of Cats", Online Edition 2004

As before, the standard introduction to category theory:

  • MacLane: "Categories for the Working Mathematician", 2nd edition, Springer 1998