COMPARING HAGINO CATEGORICAL PROGRAMMING LANGUAGE AND TYPED LAMBDA-CALCULI

Hagino (1987) develops CPL, a categorical programming language based on dialgebras which include algebras, coalgebras, products, sums and exponentials. We give an introduction to dialgebras and CPL. Working from the well-known correspondence between cartesian closed categories (CCCs) and lambda-calculi (Lambek, 1980, Curien, 1986), we study the relationship between CPL and F1, Church's simply typed lambda-calculus. We show that the reduction rules of CPL correspond to beta-reduction in first-order contexts. Iteration over inductive types may be added to F1, obtaining F(i)1 (Pierce et al., 1989). We show how to represent F(i)1 inductive types in CPL. Thus Ackermann's function is in CPL. We argue that all natural number functions N --> N provably total in first-order arithmetic can be expressed in CPL.