Strong categorical datatypes II: A term logic for categorical programming

AbstractThis paper lifts earlier category-theoretic results on datatypes to the level of an abstract language suitable for categorical programming language implementation. The earlier work built a strongly normalizing categorical combinator reduction system based entirely on functorial strength which allows the distribution of context to the interior of datatypes.Here we declare inductive (initial) and coinductive (final) datatypes in a Hagino-Wraith style to provide an expressive computing environment. An inductive (resp. coinductive) datatype consists of a strong type-forming functor accompanied by (1) a collection of constructors (resp. destructors) and (2) a fold (resp. unfold) which is parametrized by state transformations to realize the appropriate universal property.The high complexity of programming exclusively in categorical notation (combinators) warrants the development of a friendlier language isomorphic to the distributive categorical setting. In this paper such a term logic, which is also the programming language of the charity programming system, is described. This logic is first-order and is dictated directly by the underlying categorical semantics. It embodies primitive inductive and coinductive principles which reflect the uniqueness properties of the fold and unfold combinators. Several basic progam equivalences are demonstrated to illustrate how these inductive and coinductive principles can be used