TR-IIS-06-012    Fulltext

An Algebra of Dependent Data Types

Tyng-Ruey Chuang, Jan-Li Lin


We extend the standard categorical approach to algebraic data types to dependent algebraic data types, so that dependency between 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 systematic mapping of layers of categorical constructions to layers of Objective Caml modules.