A Categorical Programming Language

TL;DR

This paper introduces a new categorical framework for data types in programming languages, using F,G-dialgebras to define and reason about data structures and their duals without primitive types.

Contribution

It develops a novel categorical approach to data types with F,G-dialgebras, enabling definitions of standard and dual data types without primitive data types, and introduces a categorical programming language.

Findings

Defined data types like natural numbers and lists using F,G-dialgebras.

Proved termination of programs in the categorical language.

Provided a categorical semantics for the programming language.

Abstract

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.