A Categorical Programming Language

Tatsuya Hagino

A theory of data types based on category theory is presented. 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 programming language in a categorical
style using F,G-dialgebras as its data type declaration mechanism. We define
the meaning of the language operationally and prove that any program terminates
using Tait's computability method.