Czy istnieje izomorfizm między (podzbiorem) teorii kategorii a algebrą relacyjną?

Pochodzi z perspektywy dużych zbiorów danych. Zasadniczo wiele frameworków (takich jak Apache Spark) „kompensuje” brak operacji relacyjnych, zapewniając interfejsy podobne do Functor / Monad, i podobny ruch w kierunku konwersji kotów na SQL (Slick in Scala). Na przykład, potrzebujemy naturalnego łączenia (przy założeniu braku powtórzeń w indeksach) do elementarnego mnożenia wektorów z perspektywy SQL, co można uznać za zip + map(multiply) (MLib Spark'a już ma ElementwiseProduct) w aplikacjach Teorii Kategorii.

Po prostu (następujące przykłady są w Scali):

• odwołanie subcase od przyłączenia mogą być traktowane jako aplikacyjnej funktora (ponad klasyfikowane zbiórki), co z kolei daje nam 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). Co więcej, możemy zaindukować go do niektórych innych połączeń, zakładając pewne wstępne przetwarzanie ( groupByoperator lub po prostu podejrzenie, lub ogólnie - epimorfizm).

• inne sprzężenia i wybór można uznać za monadę. Na przykład WHEREjest po prostu: List(1,2,2,4).flatMap(x => if (x < 3) List(x) else List.empty)->List(1,2,2,4).filter(_ < 3)

• dane same w sobie to tylko ADT (GADT?), który z kolei wygląda jak prosta kategoria Set (lub bardziej ogólnie - kartezjańsko zamknięty), więc powinien (jak sądzę) obejmować operacje oparte na zestawie (z powodu Curry- Howard-Lambek sam), a także operacje takie jak RENAME(przynajmniej w praktyce).

• agregacja odpowiada fold/reduce(katamorfizm)

Pytam więc, czy możemy zbudować izomorfizm między (może podzbiorem) teorii kategorii a (całą) relacyjną algebrą, czy też jest coś odkrytego? Jeśli to działa, to jaki dokładnie „podzbiór” kategorii jest izomorficzny dla relalgebry?

Widać, że moje własne założenia są dość szerokie, a formalne rozwiązania, takie jak korespondencja Curry-Howard-Lambek dla logiki-koty-lambda, są bardziej precyzyjne - tak naprawdę proszę o odniesienie do ukończonego badania (które pokazuje bezpośredni związek ) z większą liczbą przykładów w Scala / Haskell.

Edycja : zaakceptowana odpowiedź sprawiła, że ​​pomyślałem, że posunąłem się za daleko, przedstawiając złączenia i warunki jako monadę (szczególnie używając pustej wartości, która skutecznie tworzy FAŁSZ), myślę, że wycofanie powinno wystarczyć przynajmniej dla podzbioru SQL relalgebry. Monady są lepsze do rzeczy wyższego rzędu (zagnieżdżania), takich jak GROUP BY, która nie jest częścią relalgebry.

Pozwolę sobie wyartykułować korespondencję Curry-Howarda-Lambka z odrobiną żargonu, który wyjaśnię. Lambek wykazał, że prosty typ rachunku lambda z produktami jest językiem wewnętrznym zamkniętej kartezjańskiej kategorii. Nie zamierzam wyjaśniać, czym jest zamknięta kategoria kartezjańska, chociaż nie jest to trudne, zamiast tego, jak mówi powyższe stwierdzenie, nie musisz wiedzieć! (Lub, że już wiesz, jeśli wiesz, czym jest prosty typ rachunku lambda z produktami.) Dla niektórych teorii / logiki typów bycie wewnętrznym językiem / logiką kategorii oznacza 1), że możemy zinterpretować język na strukturę kategoria w sposób, który zachowuje strukturę języka (w efekcie warunek poprawności), oraz2) i „zasadniczo” o całej strukturze wynikającej z zamknięcia kartezjańskiego można mówić w kategoriach tego języka (warunek kompletności).

$\{ x\mid x = x\}$. Każde wyrażenie algebry relacyjnej jest logicznie równoważne zapytaniu niezależnemu od domeny w rachunku relacyjnym.

Odkładając to na bok, kategorie, których wewnętrzna logika (która jest zasadniczo zdekategoryzowaną lub nieistotną formą języka wewnętrznego) są kategoriami Heyting dla intuicyjnego FOL i kategoriami logicznymi dla klasycznego FOL. (Wersje skategoryzowane / dowodowe są opisane przez hiperdoktryny . Bardzo istotne są również różnego rodzaju przedplony .) Należy zauważyć, że FOL, rachunek relacyjny i algebra relacyjna nie obsługują agregacji. (Nie obsługują również rekurencji koniecznej do przedstawienia zapytania Datalog .) Jedno podejście doGROUP BYa agregacja ma umożliwić kolumny o wartościach relacyjnych, co prowadzi do logiki wyższego rzędu (HOL) i zagnieżdżonego rachunku relacyjnego (NRC). Gdy mamy już kolumny o wartościach relacyjnych, agregację można sformalizować jako kolejny operator „skalarny”.

Twoje przykłady wskazują na fakt, że monadyczny metajęzyk jest przyzwoitym językiem dla zapytań. Artykuł Monad Compstandingions: A Versatile Representation of Queries ( PDF ) dobrze to opisuje. Bardziej wszechstronnym i nowoczesnym wyglądem jest praca doktorska Ryana Wisnesky'ego, A Functional Query Language with Categorical Types ( PDF ), która jest związana z pracą Davida Spivaka, która sama w sobie wydaje się raczej odpowiednia dla każdej interpretacji twojego pytania. (Jeśli chcesz przejść do bardziej historycznego, był Kleisli, funkcjonalny system zapytań .) W rzeczywistości monadyczny metajęzyk jest przyzwoitym językiem dla zapytań w zagnieżdżonymrachunek relacyjny. Wisnesky formułuje NRC w kategoriach elementarnego toposu, którego językiem wewnętrznym jest język Mitchell – Bénabou, który w zasadzie przypomina intuicyjną teorię zbiorów z ograniczonymi kwantyfikatorami. Dla celów Wisnesky'ego używa boolowskiego toposu, który zamiast tego będzie miał klasyczną logikę. Ten język jest jednak znacznie potężniejszy niż (rdzeń) SQL lub Datalog. Warto zauważyć, że kategoria zbiorów skończonych tworzy (logiczny) topos .