Difference between revisions of "WG211/M18Gibbons"

From WG 2.11
Jump to: navigation, search
(Created page with "'''Profunctor Optics and the Yoneda Lemma''' by Jeremy Gibbons (based on joint work with Guillaume Boisseau) ''Profunctor optics'' are a neat and composable representation of...")
 
 
(One intermediate revision by the same user not shown)
Line 1: Line 1:
'''Profunctor Optics and the Yoneda Lemma''' by Jeremy Gibbons (based on joint work with Guillaume Boisseau)
+
'''Relational Algebra by Way of Adjunctions''' by Jeremy Gibbons (based on joint work with Fritz Henglein, Ralf Hinze, and Nicolas Wu; this is an extension to the work I reported at [[WG211/M15Schedule | Meeting 15 in London]])
  
''Profunctor optics'' are a neat and composable representation of bidirectional data accessors, including lenses, and their dual, prisms. The profunctor representation exploits higher-order functions and higher-kinded type constructor classes; the relationship between this and the more familiar representation in terms of "getter" and "setter" functions is not at all obvious. We derive the profunctor representation from the concrete representation, making the relationship clear. It turns out to be a fairly direct application of the Yoneda Lemma, arguably the most important result in category theory. We hope this derivation aids understanding of the profunctor representation. Conversely, it serves to provide some insight into the Yoneda Lemma (which we will explain as we go along).
+
Bulk types such as sets, bags, and lists are monads, and therefore
 +
support a notation for database queries based on comprehensions.  This
 +
fact is the basis of much work on database query languages. The
 +
monadic structure
 +
easily
 +
explains most of standard relational
 +
algebra - specifically, selections and projections - allowing for an
 +
elegant mathematical foundation for those aspects of database query
 +
language design.
 +
Most, but not all: monads do not immediately offer an explanation of
 +
relational join or grouping,
 +
and hence important foundations for
 +
those crucial aspects of relational algebra are missing.
 +
The best they can offer is cartesian product followed by selection.
 +
Adjunctions come to the
 +
rescue: like any monad, bulk types also arise from certain adjunctions;
 +
we show that by paying due attention to other important adjunctions,
 +
we can elegantly explain the rest of standard relational algebra.
 +
In particular, this leads directly to an efficient implementation, even of
 +
joins.

Latest revision as of 11:31, 23 May 2018

Relational Algebra by Way of Adjunctions by Jeremy Gibbons (based on joint work with Fritz Henglein, Ralf Hinze, and Nicolas Wu; this is an extension to the work I reported at Meeting 15 in London)

Bulk types such as sets, bags, and lists are monads, and therefore support a notation for database queries based on comprehensions. This fact is the basis of much work on database query languages. The monadic structure easily explains most of standard relational algebra - specifically, selections and projections - allowing for an elegant mathematical foundation for those aspects of database query language design. Most, but not all: monads do not immediately offer an explanation of relational join or grouping, and hence important foundations for those crucial aspects of relational algebra are missing. The best they can offer is cartesian product followed by selection. Adjunctions come to the rescue: like any monad, bulk types also arise from certain adjunctions; we show that by paying due attention to other important adjunctions, we can elegantly explain the rest of standard relational algebra. In particular, this leads directly to an efficient implementation, even of joins.