An Algebra of Dependent Data Types

author: Tyng-Ruey Chuang and Jan-Li Lin
publication date: September 2006
cite this with: Tyng-Ruey Chuang and Jan-Li Lin. An Algebra of Dependent Data Types. Technical Report TR-IIS-06-012, Institute of Information Science, Academia Sinica. September 2006.
link this with:
copyright: all rights reserved
category: Functional Programming
full paper: pdf


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 ob ject 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 Ob jective 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 Ob jective Caml modules.

papers:tr06012:home Last modified: 2007/10/23 16:53