Algebraic Property Graphs

TL;DR

This paper formalizes algebraic property graphs using category theory and type theory, providing a unified framework for graph data models, schema transformations, and data integration in enterprise settings.

Contribution

It introduces a novel type theory for algebraic property graphs that unifies data types and schema diagrams, with theoretical guarantees for schema-based graph transformations.

Findings

Formalization of property graphs using category theory

A type theory linking algebraic data types and schema diagrams

Guarantees for schema-driven graph transformations

Abstract

We present a case study in applied category theory written from the point of view of an applied domain: the formalization of the widely-used property graphs data model in an enterprise setting using elementary constructions from type theory and category theory, including limit and co-limit sketches. Observing that algebraic data types are a common foundation of most of the enterprise schema languages we deal with in practice, for graph data or otherwise, we introduce a type theory for algebraic property graphs wherein the types denote both algebraic data types in the sense of functional programming and join-union E/R diagrams in the sense of database theory. We also provide theoretical foundations for graph transformation along schema mappings with by-construction guarantees of semantic consistency. Our data model originated as a formalization of a data integration toolkit developed at Uber which carries data and schemas along composable mappings between data interchange languages such as Apache Avro, Apache Thrift, and Protocol Buffers, and graph languages including RDF with OWL or SHACL-based schemas.