Functional database query languages as typed lambda calculi of fixed order (extended abstract)

摘要

We present a functional framework for database query languages, which 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 let abstraction; all typed using fixed order (≤ 5) functionalities. In this framework, proposed in [21] 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⁼ⁱ or simply-typed list iteration of order i+3 with equality, and MLI⁼ⁱ or ML-typed list iteration of order i+3 with equality; we use i+3 since our list representation of databases requiresat least order 3. We show that: FO-queries ⊆TLI⁼⁰ ⊆MLI⁼⁰ ⊆LOGSPACE-queries ⊆TLI⁼¹ =MLI⁼¹ = PTIME-queries ⊆ TLI2, where equality is no longer a primitive in TLI2. 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.