A simply typed lambda-calculus with types x, =>, and natural numbers can express functions N->N equivalently to those provably total in first order Peano arithmetic (cf. [Girard 89]). This encompass, e.g., the Ackermann function. Though I do not remember any reference, I do not think that more expressive power in terms of functions N->N is gained by adding other initial algebras, like List. You might also be interested in Tatsuya Hagino's categorical programming language CPL ([Hagino 87][Wraith 89][Dybkj{\ae}r 91]) which is based on (restricted) initial and final dialgebras (a dialgebra is an arrow f: F(A)->G(A) where F,G:C->D are functors). Dialgebras make it possible to define initial and final algebras, products, coproducts, and exponentials from scratch. ---Hans Dybkj{\ae}r Dybkj{\ae}r, Hans [1991]: "Category Theory, Types, and Programming Languages", PhD thesis, DIKU, University of Copenhagen, May 1991. Tecnical report 91/11. Girard, Jean-Yves, Yves Lafont, and Paul Taylor [1989]: "Proofs and Types", Cambridge University Press. Hagino, Tatsuya [1987]: "A Categorical Programming Language", PhD thesis, LFCS, University of Edinburgh, September 1987. Technical report CST-47-87. Wraith, Gavin C. [1989]: "A Note on Categorical Datatypes", in "Category Theory and Computer Science, Manchester UK, September 1989", Proceedings, edited by David H. Pitt et al., Springer-Verlag, LNCS 389. =========================================================================