In this paper, we develop an algebraic approach to data integration by combining techniques from functional programming, category theory, and database theory. In our formalism, database schemas and instances are algebraic (multi-sorted equational) theories of a certain form. Schemas denote categories, and instances denote their initial (term) algebras. The instances on a schema S form a category, S–Inst, and a morphism of schemas F : S → T induces three adjoint data migration functors: ΣF : S–Inst → T–Inst, defined by substitution along F, which has a right adjoint ΔF : T–Inst → S–Inst, which in turn has a right adjoint ΠF : S–Inst → T–Inst. We present a query language based on for/where/return syntax where each query denotes a sequence of data migration functors; a pushout-based design pattern for performing data integration using our formalism; and describe the implementation of our formalism in a tool we call AQL (Algebraic Query Language).
Functorial data migration
In this paper we present a simple database definition language: that of categories and functors. A database schema is a small category and an instance is a set-valued functor on it. We show that morphisms of schemas induce three “data migration functors”, which translate instances from one schema to the other in canonical ways. These functors parameterize projections, unions, and joins over all tables simultaneously and can be used in place of conjunctive and disjunctive queries. We also show how to connect a database and a functional programming language by introducing a functorial connection between the schema and the category of types for that language. We begin the paper with a multitude of examples to motivate the definitions, and near the end we provide a dictionary whereby one can translate database concepts into category-theoretic concepts and vice versa.
Relational foundations for functorial data migration | Proceedings of the 15th Symposium on Database Programming Languages
In this paper we present a simple database definition language: that of categories and functors. A database schema is a small category and an instance is a set-valued functor on it. We show that morphisms of schemas induce three ''data migration ...
Functional Query Languages with Categorical Types
We study three category-theoretic types in the context of functional query languages (typed lambda-calculi extended with additional operations for bulk data processing). The types we study are:
GATlab: Modeling and Programming with Generalized Algebraic Theories
Categories and categorical structures are increasingly recognized as useful abstractions for modeling in science and engineering. To uniformly implement category-theoretic mathematical models in software, we introduce GATlab, a domain-specific language for algebraic specification embedded in a technical programming language. GATlab is based on generalized algebraic theories (GATs), a logical system extending algebraic theories with dependent types so as to encompass category theory. Using GATlab, the programmer can specify generalized algebraic theories and their models, including both free models, based on symbolic expressions, and computational models, defined by arbitrary code in the host language. Moreover, the programmer can define maps between theories and use them to declaratively migrate models of one theory to models of another. In short, GATlab aims to provide a unified environment for both computer algebra and software interface design with generalized algebraic theories. In this paper, we describe the design, implementation, and applications of GATlab.
Ologs: A Categorical Framework for Knowledge Representation
In this paper we introduce the olog, or ontology log, a category-theoretic model for knowledge representation (KR). Grounded in formal mathematics, ologs can be rigorously formulated and cross-compared in ways that other KR models (such as semantic networks) cannot. An olog is similar to a relational database schema; in fact an olog can serve as a data repository if desired. Unlike database schemas, which are generally difficult to create or modify, ologs are designed to be user-friendly enough that authoring or reconfiguring an olog is a matter of course rather than a difficult chore. It is hoped that learning to author ologs is much simpler than learning a database definition language, despite their similarity. We describe ologs carefully and illustrate with many examples. As an application we show that any primitive recursive function can be described by an olog. We also show that ologs can be aligned or connected together into a larger network using functors. The various methods of information flow and institutions can then be used to integrate local and global world-views. We finish by providing several different avenues for future research.
Categorical Data Structures for Technical Computing
Many mathematical objects can be represented as functors from finitely-presented categories $\mathsf{C}$ to $\mathsf{Set}$. For instance, graphs are functors to $\mathsf{Set}$ from the category with two parallel arrows. Such functors are known informally as $\mathsf{C}$-sets. In this paper, we describe and implement an extension of $\mathsf{C}$-sets having data attributes with fixed types, such as graphs with labeled vertices or real-valued edge weights. We call such structures "acsets," short for "attributed $\mathsf{C}$-sets." Derived from previous work on algebraic databases, acsets are a joint generalization of graphs and data frames. They also encompass more elaborate graph-like objects such as wiring diagrams and Petri nets with rate constants. We develop the mathematical theory of acsets and then describe a generic implementation in the Julia programming language, which uses advanced language features to achieve performance comparable with specialized data structures.
The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits
Wiring diagrams, as seen in digital circuits, can be nested hierarchically and thus have an aspect of self-similarity. We show that wiring diagrams form the morphisms of an operad $\mcT$, capturing this self-similarity. We discuss the algebra $\Rel$ of mathematical relations on $\mcT$, and in so doing use wiring diagrams as a graphical language with which to structure queries on relational databases. We give the example of circuit diagrams as a special case. We move on to show how plug-and-play devices and also recursion can be formulated in the operadic framework as well. Throughout we include many examples and figures.
Categories for the Working Mathematician
Categories for the Working Mathematician provides an array of general ideas useful in a wide variety of fields. Starting from the foundations, this book illuminates the concepts of category, functor, natural transformation, and duality. The book then turns to adjoint functors, which provide a description of universal constructions, an analysis of the representations of functors by sets of morphisms, and a means of manipulating direct and inverse limits. These categorical concepts are extensively illustrated in the remaining chapters, which include many applications of the basic existence theorem for adjoint functors. The categories of algebraic systems are constructed from certain adjoint-like data and characterized by Beck's theorem. After considering a variety of applications, the book continues with the construction and exploitation of Kan extensions. This second edition includes a number of revisions and additions, including two new chapters on topics of active interest. One is onsymmetric monoidal categories and braided monoidal categories and the coherence theorems for them. The second describes 2-categories and the higher dimensional categories which have recently come into prominence. The bibliography has also been expanded to cover some of the many other recent advances concerning categories.
A Categorical Unification for Multi-Model Data: Part I Categorical Model and Normal Forms
Modern database systems face a significant challenge in effectively handling the Variety of data. The primary objective of this paper is to establish a unified data model and theoretical framework for multi-model data management. To achieve this, we present a categorical framework to unify three types of structured or semi-structured data: relation, XML, and graph-structured data. Utilizing the language of category theory, our framework offers a sound formal abstraction for representing these diverse data types. We extend the Entity-Relationship (ER) diagram with enriched semantic constraints, incorporating categorical ingredients such as pullback, pushout and limit. Furthermore, we develop a categorical normal form theory which is applied to category data to reduce redundancy and facilitate data maintenance. Those normal forms are applicable to relation, XML and graph data simultaneously, thereby eliminating the need for ad-hoc, model-specific definitions as found in separated normal form theories before. Finally, we discuss the connections between this new normal form framework and Boyce-Codd normal form, fourth normal form, and XML normal form.
Category Theory for Programmers: The Preface
Table of Contents Part One Category: The Essence of Composition Types and Functions Categories Great and Small Kleisli Categories Products and Coproducts Simple Algebraic Data Types Functors Functo…
Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem: ACM Transactions on Programming Languages and Systems: Vol 29, No 3
We propose a novel approach to the view-update problem for tree-structured data: a domain-specific programming language in which all expressions denote bidirectional transformations on trees. In one direction, these transformations---dubbed lenses---map ...
protolab
A patchbay for your schemas. Bidirectional data transformations, drawn as circuits.
protolab
A patchbay for your schemas. Bidirectional data transformations, drawn as circuits.
Foundations of Algebraic Specification and Formal Software Development
This book provides foundations for software specification and formal software development from the perspective of work on algebraic specification, concentrating on developing basic concepts and studying their fundamental properties. These foundations are built on a solid mathematical basis, using elements of universal algebra, category theory and logic, and this mathematical toolbox provides a convenient language for precisely formulating the concepts involved in software specification and development. Once formally defined, these notions become subject to mathematical investigation, and this interplay between mathematics and software engineering yields results that are mathematically interesting, conceptually revealing, and practically useful. The theory presented by the authors has its origins in work on algebraic specifications that started in the early 1970s, and their treatment is comprehensive. This book contains five kinds of material: the requisite mathematicalfoundations; traditional algebraic specifications; elements of the theory of institutions; formal specification and development; and proof methods. While the book is self-contained, mathematical maturity and familiarity with the problems of software engineering is required; and in the examples that directly relate to programming, the authors assume acquaintance with the concepts of functional programming. The book will be of value to researchers and advanced graduate students in the areas of programming and theoretical computer science.
Functional programming with bananas, lenses, envelopes and barbed wire
We develop a calculus for lazy functional programming based on recursion operators associated with data type definitions. For these operators we derive various algebraic laws that are useful in deriving and manipulating programs. We shall show that all example functions in Bird and Wadler's “Introduction to Functional Programming” can be expressed using these operators.
Composing schema mappings: Second-order dependencies to the rescue: ACM Transactions on Database Systems: Vol 30, No 4
A schema mapping is a specification that describes how data structured under one schema (the source schema) is to be transformed into data structured under a different schema (the target schema). A fundamental problem is composing schema mappings: given ...
