<p>A database can be viewed from two levels. The <em>physical level</em> concerns how the data is laid out in memory. The <em>logical level</em> concerns what real world entities the data describes.</p>
<p>The popular textbook <em>Database System Concepts</em> by Silberschatz, Korth, and Sudarshan describes the relation between these two layers as one of <em>abstraction</em>, 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.</p>
<p>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.</p>
<p>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 <em>secondary indexes</em>.</p>
<p>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.</p>
<p>Looking at your example, I see that tables of the <code>Project</code> type refer to keys of the <code>w</code> table. Suppose we wanted an efficient way to obtain a worker's project from their ID. We could create a table <code>worker_to_project&lt;@workers, Project&lt;workers&gt;&gt;</code> but there are some problems with this. First, we can't express the constraint that <code>worker_to_project[w].worker_id = w</code>. Additionally, suppose we added the constraint that every worker is assigned to a project. Then the <code>worker-to-project</code> map would have the same keys as the <code>workers</code> map. How would we express that constraint? And wouldn't it be awkward that we would now be applying <code>Project</code> to <code>workers</code> rather than <code>worker_to_project</code>? Why would we refer to one rather than the other given that they both have the same set of keys?</p>
<p>I think what's needed is a <em>layered schema language</em> 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 <em>indexed type systems</em>.</p>
<p>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.</p>
<pre><code>// _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 -&gt; _prop) =&gt;
union (_project : _str -&gt; _prop) =&gt;
union (_works_on : _w:_str -&gt; _prf (_worker _w) -&gt; _p:str -&gt; _prf (_project _p) -&gt; _prop)

type Project (_project_id : _str) =&gt; {
  // 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) }
}
</code></pre>
<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.</p>
<hr />
<h4>Sort Constructors</h4>
<p>(Sorts are the &quot;types&quot; that classify logical entities, a.k.a. indices, at the lower layer.)</p>
<p><strong>(_x : _sort) -&gt; _sort</strong></p>
<p>This is a dependent index-level function, where the right-hand sort may depend on the index argument <strong>_x</strong>.</p>
<h4>Type constructors</h4>
<p><strong>(_x : _sort) =&gt; Type</strong></p>
<p>Index-to-type abstraction, where the resulting type <strong>Type</strong> may depend on the index argument <strong>_x</strong>.</p>
<p><strong>{ [_x : _str] _ind : Type }</strong></p>
<p>This is a exhaustive map type, where <strong>_ind</strong> is a logical-level entity with sort <strong>_prop</strong>. Both <strong>_ind</strong> and <strong>Type</strong> can contain occurrences of <strong>_x</strong>. Values of this type contain as keys all strings <strong>_x</strong> such that the proposition <strong>_ind</strong> is true.</p>
<p><strong>{ label-1 : Type-1, ... , label-n : Type-n }</strong></p>
<p>A boring old record type</p>
<hr />
<p>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.</p>
<p>[1] <a href="https://github.com/kevinclancy/SchemaTypes/blob/main/schema_kindcheck.pdf" rel="nofollow noreferrer">https://github.com/kevinclancy/SchemaTypes/blob/main/schema_kindcheck.pdf</a></p>
<p>[2] <a href="https://github.com/kevinclancy/SchemaTypes" rel="nofollow noreferrer">https://github.com/kevinclancy/SchemaTypes</a></p>

CC BY-SA 4.0
2023-04-18T03:44:05.833Z
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
molikto
CC BY-SA 4.0
2023-04-18T03:55:39.273Z
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 ... https://github.com/UlfNorell/insane
molikto
CC BY-SA 4.0
2023-04-19T04:43:47.973Z
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?
Kevin Clancy
CC BY-SA 4.0
2023-04-19T06:16:13.697Z
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.
molikto
CC BY-SA 4.0
2023-04-21T22:42:45.167Z
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.
Kevin Clancy
CC BY-SA 4.0
2023-04-22T01:25:47.063Z
I think this will work? `{ workers: Table<auto u64, WorkerData>, worker_projects: Table<@workers, WorkerProjectData> }`
molikto
CC BY-SA 4.0
2023-04-22T01:38:05.200Z
Is the set of keys in worker_projects all workers, or just a subset of the workers? Does your formulation have a way to distinguish between the two?
Kevin Clancy
CC BY-SA 4.0
2023-04-22T01:39:34.187Z
What if each worker is involved in a set of projects? Is there a type for the set of projects that worker Bob is involved in?
Kevin Clancy
CC BY-SA 4.0
2023-04-22T01:47:21.210Z
"or just a subset of the workers" mmm.. you are right, the @workers means a subset. This seems not right. but how do you express it in SQL?
molikto
CC BY-SA 4.0
2023-04-22T01:50:26.660Z
"What if each worker is involved in a set of projects" I think just do it the traditional relational database way?


you can do `workers: Table<...>, projects: Table<...>, worker_projects: Table<{ worker: @workers, project: @projects }, {}>`


or `workers: Table<..., { projects: Table<@projects, {}> }>, projects: Table<...>`, so in this case we have a `Table` inside `Table`
molikto
CC BY-SA 4.0
2023-04-18T02:55:19.490Z
2023-05-06T22:10:12.910Z
2023-05-06T22:10:12.910Z
Kevin Clancy
<p>A database consists a list of tables. For example you have a table of <code>Worker</code> and a table of <code>Project</code> where each project needs a worker, you might express it in ordinary PLs as this:</p>
<pre><code>type Worker = { name: string } 
type Project = { name: string, worker_id: u64 }
type Database = { workers: Map&lt;u64, Worker&gt;, projects: Map&lt;u64, Project&gt; }
</code></pre>
<p>But compared to the schema in relational database, one thing is missing: you cannot express that every <code>worker_id</code> exists as a key of the <code>workers</code> map.</p>
<p>So this inspired me to add a bit dependent type to a simple type theory:</p>
<pre><code>type Worker = { name: string } 
type Project&lt;w: table&lt;Worker&gt;&gt; = { name: string, worker_id: @w }
type Database = { workers: table&lt;u64, Worker&gt;, projects: table&lt;u64, Project&lt;workers&gt;&gt; }
</code></pre>
<p>There are some new syntax</p>
<ul>
<li><code>table</code> is like a <code>Map</code> in previous code block.</li>
<li><code>w: table&lt;Worker&gt;</code> introduce a table parameter</li>
<li><code>@w</code> introduce a new type, it means the values of this type is the valid keys of <code>w</code> the table</li>
<li><code>Project&lt;workers&gt;</code> seems like a simple type generic application, but notice that the argument <code>workers</code> is a value, instead of a type. So this is a typical dependent type situation.</li>
</ul>
<p>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?)</p>
<hr />
<p>I wrote some more example here <a href="https://molikto.substack.com/publish/post/107327324" rel="nofollow noreferrer">https://molikto.substack.com/publish/post/107327324</a></p>

CC BY-SA 4.0
2023-04-19T05:14:39.590Z
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. https://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.
holf
<dependent-type><type-systems><db.databases>
Model foreign keys as dependent types?
molikto
# Model foreign keys as dependent types?

(Asked by: username_0 on 2023-04-17)

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, projects: Map }

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> = { name: string, worker_id: @w }
type Database = { workers: table, projects: table> }

There are some new syntax

table is like a Map in previous code block.
w: table 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 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://username_0.substack.com/publish/post/107327324

**Tags:** dependent-type, type-systems, db.databases

> **Comments:**
> **username_1**: 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. https://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.  

---

## 1 answers

### Answer by username_2 on 2023-04-18. Score: 2

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> 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

> **Comments:**
> **username_0**: 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 username_0 in Twitter/Discord  
> **username_0**: 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 ... https://github.com/UlfNorell/insane  
> **username_2**: 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?  
> **username_0**: 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.  
> **username_2**: 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.  
> **username_0**: I think this will work? `{ workers: Table<auto u64, WorkerData>, worker_projects: Table<@workers, WorkerProjectData> }`  
> **username_2**: Is the set of keys in worker_projects all workers, or just a subset of the workers? Does your formulation have a way to distinguish between the two?  
> **username_2**: What if each worker is involved in a set of projects? Is there a type for the set of projects that worker Bob is involved in?  
> **username_0**: "or just a subset of the workers" mmm.. you are right, the @workers means a subset. This seems not right. but how do you express it in SQL?  
> **username_0**: "What if each worker is involved in a set of projects" I think just do it the traditional relational database way?   you can do `workers: Table<...>, projects: Table<...>, worker_projects: Table<{ worker: @workers, project: @projects }, {}>`   or `workers: Table<..., { projects: Table<@projects, {}> }>, projects: Table<...>`, so in this case we have a `Table` inside `Table`  

---

