A database can be viewed from two levels. The physical level concerns how the data is laid out in memory. The logical level concerns what real world entities the data describes.
The popular textbook Database System Concepts by Silberschatz, Korth, and Sudarshan describes the relation between these two layers as one of abstraction, with the logical layer being an abstraction of the physical layer. However, I think this is a misuse of the word abstraction, and one which will lead us away from effective schema languages.
Abstraction means that we are ultimately interested in a low-level (unabstracted) object, but instead work with a more tractable high-level (abstracted) object, which is obtained from the low-level object by removing information. That's not what's going on with the logical and physical layers of a database. Instead, the logical layer (i.e. entities and relations between entities in the real world) exists independently of the physical layer. Later the physical layer is added to make statements about how the entities and relations of the logical layer are stored.
The strength of NoSQL databases such as DynamoDB is exposing the programmer to the physical layer, allowing them to organize their data in ways that permit certain queries efficiently. When the database's most common queries demand multiple distinct layouts, the data can be replicated; such replicas are referred to as secondary indexes.
Types are an effective way to describe the physical layer of NoSQL data, as the nesting structure of record and dictionary types implies a sort of spatial locality. However, as you've pointed out, standard type systems aren't capable of describing foreign key relations. Additionally, I'll point out that they aren't capable of describing the secondary indexes I've described above. The problem is that these features involve discrepancies between the logical and physical layers.
Looking at your example, I see that tables of the Project type refer to keys of the w table. Suppose we wanted an efficient way to obtain a worker's project from their ID. We could create a table worker_to_project<@workers, Project<workers>> but there are some problems with this. First, we can't express the constraint that worker_to_project[w].worker_id = w. Additionally, suppose we added the constraint that every worker is assigned to a project. Then the worker-to-project map would have the same keys as the workers map. How would we express that constraint? And wouldn't it be awkward that we would now be applying Project to workers rather than worker_to_project? Why would we refer to one rather than the other given that they both have the same set of keys?
I think what's needed is a layered schema language where the physical layer sits above (makes reference to) the logical layer. There is a formal treatment of such languages and their type systems in PL theory. They are called indexed type systems.
Here is how your example would look using a layered schema language. I've prefixed the names of logical entities with underscores to make the layered structure more visible.
// _worker is a predicate representing the set of all worker ids stored in our database
// since this is a schema, it describes all possible database instances;
// hence we take the union over all possible worker sets.
union (_worker : _str -> _prop) =>
union (_project : _str -> _prop) =>
union (_works_on : _w:_str -> _prf (_worker _w) -> _p:str -> _prf (_project _p) -> _prop)
type Project (_project_id : _str) => {
// name of the project
name : _str,
// worker tasked with working on the project. its type is a *refinement type*
// describing the subset of _str values which satisfy the _worker_id predicate
worker_id : { _x : _str | _works_on _x _project_id }
}
type Database = {
// below the workers field has a map type, but this isn't a standard map type;
// its values all have the same key set, which the set of strings that satisfy the predicate _worker
workers : { [_w : _str] (_worker _w) : Worker }
worker_to_project : { [_w : str] (_worker _w) : { _p : str | (_works_on _w _p) } }
projects : { [_p : _str] (_project _p) : (Project _p) }
}
Here is a glossary of the constructs involved. I neglected to distinguish metavariables from the object language, but I'll fix that at some point. For now, if you want to see a more rigorous presentation then look at the linked paper.
Sort Constructors
(Sorts are the "types" that classify logical entities, a.k.a. indices, at the lower layer.)
(_x : _sort) -> _sort
This is a dependent index-level function, where the right-hand sort may depend on the index argument _x.
Type constructors
(_x : _sort) => Type
Index-to-type abstraction, where the resulting type Type may depend on the index argument _x.
{ [_x : _str] _ind : Type }
This is a exhaustive map type, where _ind is a logical-level entity with sort _prop. Both _ind and Type can contain occurrences of _x. Values of this type contain as keys all strings _x such that the proposition _ind is true.
{ label-1 : Type-1, ... , label-n : Type-n }
A boring old record type
I've formalized typing rules and instrinsic categorical semantics for such a language in a pdf [1]. I created a github repo containing a prototype validator for this schema language[2], targeted at MUMPS/Objectscript databases. This project has been on hold for awhile, as I've been busy with work. I never got around to formalizing a connection between the validator and the language semantics.
[1] https://github.com/kevinclancy/SchemaTypes/blob/main/schema_kindcheck.pdf
[2] https://github.com/kevinclancy/SchemaTypes
