One of the main challenges of building an enterprise knowledge graph is guaranteeing interoperability between a single graph data model and the diverse and often changeable ecosystem of non-graph data models, languages, and tools which surround and support the graph. The simple and developer-friendly property graph family of data models lends itself to this task, yet the lack of a formal specification deprives the graph of well-defined semantics. In this paper, we observe that algebraic data types are a common foundation of most of the enterprise schema languages we deal with in practice, and are also a suitable basis for a property graph formalism. We introduce this formalism in terms of type theory, algebra, and category theory, also providing algorithms for query processing and data migration with guarantees of semantic consistency across supported languages and datasets. These results have clear connections to relational database theory, programming language theory, and graph theory, providing starting points for significant future work. Open research challenges described in the paper include adding constraints, query and schema languages, and logics on top of the basic type system, interfacing with specific graph and non-graph data models, and performing operations which are typically difficult or ill-defined on property graphs, such as graph merges.