A Categorical Programming Language

The work

AuthorsTatsuya Hagino
Editors
Typephdthesis
Year1987
Citekeyhagino1987categorical

Where it appeared

PublisherUniversity of Edinburgh

Identifiers

arXiv2010.05167 from its doi
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.

A copy is held

pdf, 860.5 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-07 14:51 UTC

Filed under

the-copy-is-not-the-work what-a-program-means

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},
}

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