Existe-t-il un isomorphisme entre (un sous-ensemble de) la théorie des catégories et l'algèbre relationnelle?

Cela vient du Big Data. Fondamentalement, de nombreux frameworks (comme Apache Spark) "compensent" le manque d'opérations relationnelles en fournissant des interfaces de type Functor / Monad et il existe un mouvement similaire vers les conversions de chats en SQL (Slick in Scala). Par exemple, nous avons besoin d'une jointure naturelle (en supposant qu'il n'y ait pas de répétitions sur les index) pour la multiplication par élément des vecteurs du point de vue SQL, qui pourrait être considérée comme zip + map(multiply) (la MLib de Spark en a déjà ElementwiseProduct) dans les applications de la théorie des catégories.

Dire simplement (les exemples suivants sont en Scala):

• le sous-cas référencé de jointure peut être pensé comme foncteur applicatif (sur collection triée), ce qui à son tour nous donne 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). De plus, nous pouvons l'induire à d'autres jointures, en supposant un prétraitement ( groupByopérateur ou simplement surjection, ou généralement - un épimorphisme).

• les autres jointures et sélections peuvent être considérées comme une monade. Par exemple, WHEREc'est juste: List(1,2,2,4).flatMap(x => if (x < 3) List(x) else List.empty)->List(1,2,2,4).filter(_ < 3)

• les données elles-mêmes sont juste ADT (GADT aussi?), qui à son tour ressemble à une simple catégorie Set (ou plus généralement - cartésienne fermée), donc elle devrait (je suppose) couvrir les opérations basées sur Set (en raison de Curry- Howard-Lambek lui-même) et aussi des opérations comme RENAME(au moins dans la pratique).

• l'agrégation correspond à fold/reduce(catamorphisme)

Donc, ce que je demande, c'est peut-on construire un isomorphisme entre (peut-être un sous-ensemble de) la théorie des catégories et (toute) l'algèbre relationnelle ou y a-t-il quelque chose à découvrir? Si cela fonctionne, quel "sous-ensemble" exact de catégories est isomorphe à la relalgèbre?

Vous pouvez voir que mes propres hypothèses sont assez larges tandis que les solutions formelles comme la correspondance Curry-Howard-Lambek pour logic-cats-lambda sont plus précises - donc en fait, je demande une référence à une étude accomplie (qui montre une relation directe ) avec plus d'exemples dans Scala / Haskell.

Edit : la réponse acceptée m'a fait penser que j'allais trop loin en représentant les jointures et les conditions en tant que monade (en particulier en utilisant une valeur vide qui instancie efficacement FALSE), je pense que les retraits devraient suffire au moins pour le sous-ensemble de relalgebra de SQL. Les monades sont meilleures pour les trucs d'ordre supérieur (imbrication) comme GROUP BY, qui ne fait pas partie des relalgebra.

Permettez-moi d'articuler la correspondance Curry-Howard-Lambek avec un peu de jargon que je vais expliquer. Lambek a montré que le calcul lambda simplement tapé avec des produits était le langage interne d'une catégorie fermée cartésienne. Je ne vais pas expliquer ce qu'est une catégorie fermée cartésienne, bien que ce ne soit pas difficile, mais ce que dit la déclaration ci-dessus, c'est que vous n'avez pas besoin de savoir! (Ou que vous savez déjà, si vous savez ce qu'est le calcul lambda simplement tapé avec des produits.) Pour qu'une théorie / logique de type soit le langage / la logique interne d'une catégorie signifie 1) que nous pouvons interpréter le langage dans la structure sur la catégorie d'une manière qui préserve la structure de la langue (en fait une condition de solidité), et2) et "essentiellement" toute la structure issue de la fermeture cartésienne peut être évoquée en termes de ce langage (condition d'exhaustivité).

$\{ x\mid x = x\}$. Chaque expression d'algèbre relationnelle est logiquement équivalente à une requête indépendante du domaine dans le calcul relationnel.

Mis à part cela, les catégories dont la logique interne (qui est essentiellement une forme décatégorifiée ou non pertinente d'un langage interne) sont les catégories de Heyting pour le FOL intuitionniste et les catégories booléennes pour le FOL classique. (Les versions pertinentes catégorisées / preuves sont décrites par des hyperdoctrines . Les prétoposes de diverses sortes sont également très pertinentes .) Notez que le FOL, le calcul relationnel et l'algèbre relationnelle ne prennent pas en charge l'agrégation. (Ils ne prennent pas non plus en charge la récursivité nécessaire pour représenter une requête Datalog .) Une approche pourGROUP BYet l'agrégation consiste à autoriser les colonnes à valeur relationnelle qui conduisent à une logique d'ordre supérieur (HOL) et au calcul relationnel imbriqué (NRC). Une fois que nous avons des colonnes à valeurs relationnelles, l'agrégation peut être formalisée comme un autre opérateur "scalaire".

Vos exemples soulignent le fait qu'un méta-langage monadique est un langage décent pour les requêtes. Le document Monad Comprehensions: A Versatile Representation of Queries ( PDF ) l'explique bien. Un aspect plus complet et moderne est la thèse de doctorat de Ryan Wisnesky, A Functional Query Language with Categorical Types ( PDF ), qui est liée au travail de David Spivak qui lui-même semble plutôt pertinent pour toute interprétation de votre question. (Si vous voulez aller plus historique, il y avait le Kleisli, un système de requête fonctionnel .) En fait, le méta-langage monadique est un langage décent pour les requêtes dans le nestedcalcul relationnel. Wisnesky formule le NRC en termes de topos élémentaires dont le langage interne est le langage Mitchell-Bénabou qui ressemble fondamentalement à une théorie des ensembles intuitionniste avec des quantificateurs bornés. Pour les besoins de Wisnesky, il utilise un topos booléen qui aura plutôt une logique classique. Ce langage est cependant beaucoup plus puissant que SQL (Datalog) ou Datalog. Il convient de noter que la catégorie des ensembles finis forme un topos (booléen) .