Existe um isomorfismo entre (subconjunto de) teoria de categorias e álgebra relacional?

Vem da perspectiva do big data. Basicamente, muitas estruturas (como o Apache Spark) "compensam" a falta de operações relacionais, fornecendo interfaces do tipo Functor / Monad e há um movimento semelhante em relação às conversões de gatos para SQL (Slick in Scala). Por exemplo, precisamos de junção natural (assumindo que não há repetições nos índices) para multiplicar elementos de vetores da perspectiva SQL, que pode ser considerada como zip + map(multiply) (o MLib do Spark, no entanto, já possui ElementwiseProduct) nas aplicações da Teoria da Categoria.

Simplesmente dizendo (os seguintes exemplos estão em Scala):

• a subcaixa referenciada de junção pode ser pensada como um functor aplicativo (sobre coleção ordenada), que por sua vez nos fornece 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). Além disso, podemos induzi-lo a outras junções, assumindo algum pré-processamento ( groupByoperador ou apenas rejeição, ou geralmente - um epimorfismo).

• outras junções e seleção podem ser pensadas como mônada. Por exemplo, WHEREé apenas: List(1,2,2,4).flatMap(x => if (x < 3) List(x) else List.empty)->List(1,2,2,4).filter(_ < 3)

• os dados em si são apenas ADT (GADT também?), que, por sua vez, se parece com uma simples categoria Set (ou, de um modo geral, fechado por Cartesiano), portanto deve (suponho) cobrir operações baseadas em Set (devido a Curry- Howard-Lambek em si) e também operações como RENAME(pelo menos na prática).

• agregação corresponde a fold/reduce(catamorfismo)

Então, o que estou perguntando é: podemos construir um isomorfismo entre (talvez um subconjunto da) teoria das categorias e (todo) a álgebra relacional ou há algo descoberto? Se funcionar, que "subconjunto" exato de categorias é isomórfico para relalgebra?

Você pode ver que minhas próprias suposições são bastante amplas, enquanto soluções formais como a correspondência de Curry-Howard-Lambek para lógica-gatos-lambda são mais precisas - então, na verdade, estou pedindo uma referência a um estudo realizado (que mostra uma relação direta ) com mais exemplos em Scala / Haskell.

Edit : a resposta aceita me fez pensar que eu fui longe demais representando junções e condições como uma mônada (especialmente usando um valor vazio que efetivamente instancia FALSE), acho que retrocessos devem ser suficientes pelo menos para o subconjunto relalgebra do SQL. Mônadas são melhores para coisas de ordem superior (agrupamento), como GROUP BY, que não faz parte do relalgebra.

Deixe-me articular a correspondência de Curry-Howard-Lambek com um pouco de jargão que eu explicarei. Lambek mostrou que o cálculo lambda simplesmente digitado com produtos era o idioma interno de uma categoria fechada cartesiana. Não vou explicar o que é uma categoria fechada cartesiana, embora não seja difícil. Em vez disso, o que a declaração acima diz é que você não precisa saber! (Ou você já sabe, se você sabe o que é o cálculo lambda simplesmente digitado com produtos.) Para algum tipo teoria / lógica, ser a linguagem / lógica interna de uma categoria significa 1) que podemos interpretar a linguagem na estrutura em a categoria de maneira a preservar a estrutura do idioma (na verdade, uma condição de solidez), e2) e "essencialmente" toda a estrutura resultante do fechamento cartesiano pode ser discutida em termos dessa linguagem (uma condição de completude).

A álgebra relacional é equivalente ao cálculo relacional de tupla ou domínio, que é essencialmente lógica de primeira ordem. Essa afirmação é aproximadamente o teorema de Codd , embora um teorema semelhante tenha sido provado décadas antes por Tarski para FOL e álgebras cilíndricas . Há um pouco de sutileza, no entanto. Queremos que as consultas no cálculo relacional sejam independentes de domínio, ou seja, expandir o domínio de valores possíveis não altera os resultados de uma consulta. Um exemplo de uma consulta de cálculo relacional que não é independente do domínio é . Toda expressão de álgebra relacional é logicamente equivalente a um domínio independente$\{ x\mid x = x\}$ consulta no cálculo relacional.

Colocando isso de lado, as categorias cuja lógica interna (que é essencialmente uma forma decategorificada ou irrelevante de uma linguagem interna) são categorias de Heyting para as categorias FOL intuicionistas e Booleanas para as FOL clássicas. (As versões relevantes categorified / prova são descritas por hyperdoctrines . Também são muito relevantes pretoposes de vários tipos.) Note, que FOL, o cálculo relacional e álgebra relacional que não suportam a agregação. (Eles também não suportam a recursão necessária para representar uma consulta do registro de dados.)GROUP BYe agregação é permitir colunas com valor de relação que levam à lógica de ordem superior (HOL) e ao cálculo relacional aninhado (NRC). Depois de termos colunas com valor de relação, a agregação pode ser formalizada como apenas mais um operador "escalar".

Seus exemplos apontam para o fato de que uma meta-linguagem monádica é uma linguagem decente para consultas. O artigo Compreensões da Mônada: Uma Representação Versátil de Consultas ( PDF ) explica isso bem. Uma aparência mais abrangente e moderna é a tese de doutorado de Ryan Wisnesky, Uma linguagem de consulta funcional com tipos categóricos ( PDF ), relacionada ao trabalho de David Spivak, que por si só parece bastante relevante para qualquer interpretação da sua pergunta. (Se você quiser se tornar mais histórico, havia o Kleisli, um sistema de consulta funcional .) De fato, a meta-linguagem monádica é uma linguagem decente para consultas no diretório aninhado.cálculo relacional. Wisnesky formula NRC em termos de topos elementares cuja linguagem interna é a linguagem Mitchell-Bénabou, que basicamente se parece com uma teoria de conjuntos intuicionista com quantificadores limitados. Para o propósito de Wisnesky, ele usa um topos booleanos que terão uma lógica clássica. Essa linguagem é muito mais poderosa do que o SQL ou o Datalog (principal). Vale ressaltar que a categoria de conjuntos finitos forma um topos (booleanos) .