Is there an isomorphism between (subset of) category theory and relational algebra?

Question

It comes from big data perspective. Basically, many frameworks (like Apache Spark) "compensate" lack of relational operations by providing Functor/Monad-like interfaces and there is a similar movement towards cats-to-SQL conversions (Slick in Scala). For instance, we need natural join (assuming no repetitions on indexes) for element-wise multiplication of vectors from SQL-perspective, which could be considered as zip + map(multiply) (Spark's MLib, however, already has ElementwiseProduct) in Category Theory's applications.

Simply saying (following examples are in Scala):

• the referenced subcase of join can be thought as applicative functor (over sorted collection), which in its turn gives us zip: List(1,2,3).ap(List(2,4,8).map(a => (b: Int) => a * b)) --> (List(1,2,3) zip List(2,4,8)).map(x => x._1 * x._2). Moreover, we can induce it to some other joins, assuming some preprocessing (groupBy operator or just surjection, or generally - an epimorphism).

• other joins and selection can be thought as monad. For instance, WHERE is just: List(1,2,2,4).flatMap(x => if (x < 3) List(x) else List.empty) --> List(1,2,2,4).filter(_ < 3)

• data itself is just ADT (GADT too?), which in its turn looks like a simple Set-category (or more generally speaking - Cartesian-closed), so it should (I suppose) cover Set-based operations (due to Curry-Howard-Lambek itself) and also operations like RENAME (at least in practice).

• aggregation corresponds to fold/reduce (catamorphism)

So, what I'm asking is can we build an isomorphism between (maybe subset of) category theory and (the whole) relational algebra or is there something uncovered? If it works, what exact "subset" of categories is isomorphic to relalgebra?

You can see that my own assumptions are quite broad while formal solutions like Curry-Howard-Lambek correspondence for logic-cats-lambda are more precise - so actually, I'm asking for a reference to an accomplished study (that shows a direct relationship) with more examples in Scala/Haskell.

Edit: the accepted answer made me think that I went too far representing joins and conditions as a monad (especially using an empty value that effectively instantiates FALSE), I think pullbacks should suffice at least for relalgebra subset of SQL. Monads are better for higher order (nesting) stuff like GROUP BY, which isn’t part of relalgebra.

Answer 1

Let me articulate the Curry-Howard-Lambek correspondence with a bit of jargon which I'll explain. Lambek showed that the simply typed lambda calculus with products was the internal language of a cartesian closed category. I'm not going to spell out what a cartesian closed category is, though it isn't difficult, instead what the above statement says is you don't need to know! (Or that you already know, if you know what the simply typed lambda calculus with products is.) For some type theory/logic to be the internal language/logic of a category means 1) that we can interpret the language into the structure on the category in a way that preserves the structure of the language (in effect a soundness condition), and 2) and "essentially" all the structure arising from cartesian closure can be talked about in terms of this language (a completeness condition).

The relational algebra is equivalent to the tuple or domain relational calculus which is essentially first order logic. This statement is roughly Codd's theorem, though a similar theorem was proved decades earlier by Tarski for FOL and cylindrical algebras. There is a bit of a subtlety though. We want the queries in the relational calculus to be domain independent, which is to say that expanding the domain of possible values doesn't change the results of a query. An example of a relational calculus query that is not domain independent is $\{ x\mid x = x\}$. Every relational algebra expression is logically equivalent to a domain independent query in relational calculus.

Putting that aside, the categories whose internal logic (which is essentially a decategorified or proof-irrelevant form of an internal language) are Heyting categories for intuitionistic FOL and Boolean categories for classical FOL. (The categorified/proof relevant versions are described by hyperdoctrines. Also very relevant are pretoposes of various sorts.) Note, that FOL, the relational calculus, and the relational algebra do not support aggregation. (They also don't support the recursion necessary to represent a Datalog query.) One approach to GROUP BY and aggregation is to allow relation-valued columns which leads to higher-order logic (HOL) and the nested relational calculus (NRC). Once we have relation-valued columns, aggregation can be formalized as just another "scalar" operator.

Your examples point to the fact that a monadic meta-language is a decent language for queries. The paper Monad Comprehensions: A Versatile Representation of Queries (PDF) spells this out well. A more comprehensive and modern look is Ryan Wisnesky's PhD thesis, A Functional Query Language with Categorical Types (PDF), which is related to David Spivak's work which itself seems rather relevant to any interpretation of your question. (If you want to go more historical, there was the Kleisli, A Functional Query System.) In fact, the monadic meta-language is a decent language for queries in the nested relational calculus. Wisnesky formulates NRC in terms of an elementary topos whose internal language is the Mitchell–Bénabou language which basically looks like an intuitionistic set theory with bounded quantifiers. For Wisnesky's purpose, he uses a Boolean topos which will instead have a classical logic. This language is quite a lot more powerful than (core) SQL or Datalog though. It is worth noting that the category of finite sets forms a (Boolean) topos.