A database consists a list of tables. For example you have a table of Worker and a table of Project where each project needs a worker, you might express it in ordinary PLs as this:

type Worker = { name: string } 
type Project = { name: string, worker_id: u64 }
type Database = { workers: Map<u64, Worker>, projects: Map<u64, Project> }

But compared to the schema in relational database, one thing is missing: you cannot express that every worker_id exists as a key of the workers map.

So this inspired me to add a bit dependent type to a simple type theory:

type Worker = { name: string } 
type Project<w: table<Worker>> = { name: string, worker_id: @w }
type Database = { workers: table<u64, Worker>, projects: table<u64, Project<workers>> }

There are some new syntax

  • table is like a Map in previous code block.
  • w: table<Worker> introduce a table parameter
  • @w introduce a new type, it means the values of this type is the valid keys of w the table
  • Project<workers> seems like a simple type generic application, but notice that the argument workers is a value, instead of a type. So this is a typical dependent type situation.

Is this idea explored before? What do you think of this? Can it be expanded to a full-featured relational language but looks like ordinary PLs? (indexes, incrementally maintained views?, what other features?)

I wrote some more example here https://molikto.substack.com/publish/post/107327324

  • $\begingroup$ I am far from knowledgeable on this but you could have a look at SQLCert, a Coq certification of SQL and of a query planner. The paper "V. Benzaken , E. Contejean and S. Dumbrava : A Coq Formalization of the Relational Data Model in ESOP 2014" mentions the encoding of integrity constraints. datacert.lri.fr/sqlcert contains some doc. For the rest, I do not really know, you could ask Evelyne Coutejean or Véronique Benzaken who led the project. $\endgroup$
    – holf
    Apr 19, 2023 at 5:14

1 Answer 1


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

  • $\begingroup$ Thx! I feel your formulation is a bit more complicated because of the seprate index language, but we are thinking about the exact same problem! If you want to chat or collaborate, I am molikto in Twitter/Discord $\endgroup$
    – molikto
    Apr 18, 2023 at 3:44
  • $\begingroup$ Can you elaborate what's bad with my formulation? One thing I can think of is mutually referencing tables means each field in a record type can dependent on each other, so it's insane ... github.com/UlfNorell/insane $\endgroup$
    – molikto
    Apr 18, 2023 at 3:55
  • $\begingroup$ Sure, I'd be glad to collaborate. I don't use twitter or discord, but I'll send you an email at some point. As for what's wrong with your formulation, I'll have to think about this. It seems awkward to me to parameterize the Project type by an entire table when really you only care about its keys. Can your formulation represent indexes? $\endgroup$ Apr 19, 2023 at 4:43
  • $\begingroup$ Yes. The over parametrization is a problem. The idea is this enable you have a modular database (you can reuse a type by binding to different table, or create container types (e.g. trees) that accept a table parameter. $\endgroup$
    – molikto
    Apr 19, 2023 at 6:16
  • $\begingroup$ What if you had two tables with the set of all workers as keys? One mapping a worker to their personal data and another to their project. A "worker" foreign key can be used to index either table, but your system requires the programmer to refer to one and not the other to express a foreign key. That doesn't seem ideal to me. And we can't express that the two tables have the same set of keys. $\endgroup$ Apr 21, 2023 at 22:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.