What John calls databases are actually constant lookup structures, whereas real-life databases are all about modifying such structures efficiently!

> When you enter data, you have to check this equation!

In this discussion, entering data means changing the functor! In fact, adding data means adding equations! And 'checking' means taking care that our new equations don't contradict ones that are already present.

If we want to reason about changing databases we'll have to introduce even higher kinds of functions! So far we have a functor I which creates a dataset from a schema:

\\[ I: C \rightarrow Gr(I) \\]

To make I encompass more data we need to apply a higher functor (a natural transformation) to I:

\\[ A: I \rightarrow I \\]

In real life, we'd parametrize A such that we can give the data record to be added as extra parameter:

\\[ insert: record \rightarrow I \rightarrow I \\]

Deleting stuff is quite popular:

\\[ delete: index \rightarrow I \rightarrow I \\]

Their combination is also very common, and having more primitives can help to make operations more efficient:

\\[ replace: index \rightarrow record \rightarrow I \rightarrow I \\]

Btw, I'm not quite sure how to express a selector like 'index' using categories. It seems it should be a schema including equations, like C, and compatible to it, but with more restrictions, so it matches (or rather the instanciation functor I produces) a subset of the whole.

Puzzle rf39.1: How should I write this? Should I mention our functor I? Is the following inclusion pointing in the right direction?

\\[ C' \subset C \\]

For now, let's assume C' encodes constraints as intended. In practice we'll further see querying as a primitive:

\\[ select: C' \rightarrow I \rightarrow Gr'(I) \\]

Once we can do that, we can give a series of similar changes very succinctly:

\\[ update: C' \rightarrow I' \rightarrow I' \rightarrow I \rightarrow I \\]

Okay, I'm really not sure how to do this, but I'm confident that this stuff will be part of a future lecture, possibly one titled 'natural transformations'...

> When you enter data, you have to check this equation!

In this discussion, entering data means changing the functor! In fact, adding data means adding equations! And 'checking' means taking care that our new equations don't contradict ones that are already present.

If we want to reason about changing databases we'll have to introduce even higher kinds of functions! So far we have a functor I which creates a dataset from a schema:

\\[ I: C \rightarrow Gr(I) \\]

To make I encompass more data we need to apply a higher functor (a natural transformation) to I:

\\[ A: I \rightarrow I \\]

In real life, we'd parametrize A such that we can give the data record to be added as extra parameter:

\\[ insert: record \rightarrow I \rightarrow I \\]

Deleting stuff is quite popular:

\\[ delete: index \rightarrow I \rightarrow I \\]

Their combination is also very common, and having more primitives can help to make operations more efficient:

\\[ replace: index \rightarrow record \rightarrow I \rightarrow I \\]

Btw, I'm not quite sure how to express a selector like 'index' using categories. It seems it should be a schema including equations, like C, and compatible to it, but with more restrictions, so it matches (or rather the instanciation functor I produces) a subset of the whole.

Puzzle rf39.1: How should I write this? Should I mention our functor I? Is the following inclusion pointing in the right direction?

\\[ C' \subset C \\]

For now, let's assume C' encodes constraints as intended. In practice we'll further see querying as a primitive:

\\[ select: C' \rightarrow I \rightarrow Gr'(I) \\]

Once we can do that, we can give a series of similar changes very succinctly:

\\[ update: C' \rightarrow I' \rightarrow I' \rightarrow I \rightarrow I \\]

Okay, I'm really not sure how to do this, but I'm confident that this stuff will be part of a future lecture, possibly one titled 'natural transformations'...