Relational Algebra by Way of Adjunctions
Jeremy Gibbons‚ Fritz Henglein‚ Ralf Hinze and Nicolas Wu
A seminal observation made by Wadler and Trinder and subsequently by Buneman and Wong in the early 1990s was that bulk types are monads, and therefore support a notation for database queries based on comprehensions. This observation formed the basis of Wong's Kleisli language, and later Wadler's Links language. The monadic structure explains most of standard relational algebra, allowing for an elegant mathematical foundation for those aspects of database query language design. Unfortunately, monads per se offer no explanation of cartesian product, and hence provide no foundations for the crucial aspect of relational joins. But the monadic structure of bulk types (like any monad) arises from one specific adjunction; we show that by paying due attention to other important adjunctions we can elegantly explain the rest of standard relational algebra, in a way that leads directly to an efficient implementation.