A Categorical Programming Language

The work

TitleA Categorical Programming Language
AuthorsTatsuya Hagino
TypePhD thesis
Year1987
Citekeyhagino1987categorical

Where it appeared

PublisherUniversity of Edinburgh

Identifiers

DOI10.48550/arxiv.2010.05167
OpenAlexW2164343886

Access

Landing pagehttp://arxiv.org/abs/2010.05167
Free full texthttps://arxiv.org/pdf/2010.05167

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.

Copy held

KindPDF, 881.1 kB
Retrieved2026-08-07
Heldlocal, for personal reference
Where it came fromhttps://arxiv.org/pdf/2010.05167

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Standingendorsed
Approved2026-08-07

Cite it as

@phdthesis{hagino1987categorical,
  title = {A Categorical Programming Language},
  author = {Tatsuya Hagino},
  year = {1987},
  publisher = {University of Edinburgh},
  doi = {10.48550/arxiv.2010.05167},
  url = {https://arxiv.org/pdf/2010.05167},
}

This record lives at https://refs.drheap.org/hagino1987categorical/ and will keep doing so.