## A Categorical Programming Language

**Tatsuya Hagino**
*Abstract:* A theory of data types and a programming
language based on category theory are presented.

Data types play a crucial role in programming. They enable us to
write programs easily and elegantly. Various programming languages
have been developed, each of which may use different kinds of data
types. Therefore, it becomes important to organize data types
systematically so that we can understand the relationship between
one data type and another and investigate future directions which
lead us to discover exciting new data types.

There have been several approaches to systematically organize
data types: algebraic specification methods using algebras, domain
theory using complete partially ordered sets and type theory using
the connection between logics and data types. Here, we use category
theory. Category theory has proved to be remarkably good at
revealing the nature of mathematical objects, and we use it to
understand the true nature of data types in programming.

We organize data types under a new categorical notion of
*F,G-dialgebras* which is an extension of the notion of
adjunctions as well as that of *T-algebras*. *T*-algebras
are also used in domain theory, but while domain theory needs some
primitive data types, like products, to start with, we do not need
any. Products, coproducts and exponentiations (i.e. function
spaces) are defined exactly like in category theory using
adjunctions. *F,G*-dialgebras also enable us to define the
natural number object, the object for finite lists and other
familiar data types in programming. Furthermore, their symmetry
allows us to have the dual of the natural number object and the
object for infinite lists (or lazy lists).

We also introduce a functional programming language in a
categorical style. It has no primitive data types nor primitive
control structures. Data types are declared using
*F,G*-dialgebras and each data type is associated with its own
control structure. For example, natural numbers are associated with
primitive recursion. We define the meaning of the language
operationally by giving a set of reduction rules. We also prove
that any computation in this programming language terminates using
Tait's computability method.

A specification language to describe categories is also
included. It is used to give a formal semantics to
*F,G*-dialgebras as well as to give a basis to the categorical
programming language we introduce.

**Ph.D. thesis - Price £7.00**

*LFCS report ECS-LFCS-87-38*

Previous |

Index |

Next