Algebraic Property Graphs
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.