Functional Database Query Languages as Typed Lambda Calculi of Fixed Order

We present a functional framework for database query languages that is analogous to the conventional logical framework of first-order and fixpoint formulas over finite structures. We use atomic constants of order~0, equality among these constants, variables, application, lambda abstraction, and {\tt let} abstraction; all typed using fixed order ($\leq 5$) functionalities. In this framework, proposed in [HKM93] for arbitrary order functionalities, queries and databases are both typed lambda terms, evaluation is by reduction, and the main programming technique is list iteration. We define two families of languages: TLI$^=_i$ or simply-typed list iteration of order~$i+3$ with equality, and MLI$^=_i$ or ML-typed list iteration of order~$i+3$ with equality; we use $i+3$ since our list representation of databases requires at least order~3. We show that: $\hbox{FO-queries} \subseteq \hbox{TLI}^=_0 \subseteq \hbox{MLI}^=_0 \subseteq \hbox{LOGSPACE-queries} \subseteq \hbox{TLI}^=_1 = \hbox{MLI}^=_1 = \hbox{PTIME-queries} \subseteq \hbox{TLI}_2$, where equality is no longer a primitive in TLI$_2$. We also show that ML type inference, restricted to fixed order, is polynomial in the size of the program typed. Since programming by using low order functionalities and type inference is common in functional languages, our results indicate that such programs suffice for expressing efficient computations and that their ML-types can be efficiently inferred.