Functorial data migration

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 ...

Algebraic data integration

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).

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.

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:

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…

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.

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.

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.

Profunctor Optics, a Categorical Update

Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.

Coeffects: a calculus of context-dependent computation

The notion of context in functional languages no longer refers just to variables in scope. Context can capture additional properties of variables (usage patterns in linear logics; caching requirements in dataflow languages) as well as additional resources or properties of the execution environment (rebindable resources; platform version in a cross-platform application). The recently introduced notion of coeffects captures the latter, whole-context properties, but it failed to capture fine-grained per-variable properties.We remedy this by developing a generalized coeffect system with annotations indexed by a coeffect shape. By instantiating a concrete shape, our system captures previously studied flat (whole-context) coeffects, but also structural (per-variable) coeffects, making coeffect analyses more useful. We show that the structural system enjoys desirable syntactic properties and we give a categorical semantics using extended notions of indexed comonad.The examples presented in this paper are based on analysis of established language features (liveness, linear logics, dataflow, dynamic scoping) and we argue that such context-aware properties will also be useful for future development of languages for increasingly heterogeneous and distributed platforms.

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 ...

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.

A categorical manifesto

This paper tries to explain why and how category theory is useful in computing science, by giving guidelines for applying seven basic categorical concepts: category, functor, natural transformation, limit, adjoint, colimit and comma category. Some examples, intuition, and references are given for each concept, but completeness is not attempted. Some additional categorical concepts and some suggestions for further research are also mentioned. The paper concludes with some philosophical discussion.

Bidirectional Programming Languages

The need to edit source data through a view arises in a host of applications across many different areas of computing. Unfortunately, few existing systems provide support for updatable views. In practice, when they are needed, updatable views are usually implemented using two separate programs: one that computes the view from the source and another that handles updates. This rudimentary design is tedious for programmers, difficult to reason about, and a nightmare to maintain. This dissertation presents bidirectional programming languages, which provide an elegant and effective mechanism for describing updatable views. Unlike programs written in an ordinary language, which only work in one direction, programs in a bidirectional language can be run both forwards and backwards: from left to right, they describe functions that map sources to views, and from right to left, they describe functions that map updated views back to updated sources. Besides eliminating redundancy, these languages can be designed to ensure correctness, guaranteeing by construction that the two functions work well together. Starting from the foundations, we define a general semantic space of well-behaved bidirectional transformations called lenses. Then, building on this foundation, we describe a particular language for defining lenses on strings with syntax based on the familiar regular operators (union, concatenation, and Kleene star). We present extensions to the basic framework that address the subtle complications that arise when lenses are used to manipulate, data containing unimportant details, ordered data, and confidential data.

Graceful database schema evolution: the PRISM workbench: Proceedings of the VLDB Endowment: Vol 1, No 1

Supporting graceful schema evolution represents an unsolved problem for traditional information systems that is further exacerbated in web information systems, such as Wikipedia and public scientific databases: in these projects based on multiparty ...

Basic Category Theory

This short introductory category theory textbook is for readers with relatively little mathematical background (e.g. the first half of an undergraduate mathematics degree). At its heart is the concept of a universal property, important throughout mathematics. After a chapter introducing the basic definitions, separate chapters present three ways of expressing universal properties: via adjoint functors, representable functors, and limits. A final chapter ties the three together. For each new categorical concept, a generous supply of examples is provided, taken from different parts of mathematics. At points where the leap in abstraction is particularly great (such as the Yoneda lemma), the reader will find careful and extensive explanations.