An Algebra of Dependent Data Types

Abstract. We extend the standard categorical approach to algebraic data types to dependent algebraic data types, so that dependency be-tween two algebraic data types has natural semantics. Specifically, for two inductive data types S and A characterized by two F-algebra F and G, any natural transformation η: F → G gives rise to a dependency of S on A. This natural dependency is the initial object of what we call a Fη-algebra. The initiality further allows us to describe certain dependencies in functions that both involve S and A. We have used Objective Caml to write functional programs where dependencies among data types (and in the relevant functions) are made explicit. This is done by a system-atic mapping of layers of categorical constructions to layers of Objective Caml modules.