mathetic

I used natural numbers as a simplification. In full generality, you can use a lattice where min and max are replaced by meet and join operations. Then you can have categories that are not comparable to each other.

As for privacy, you definitely have security levels. For example, think of employee record system in a simple company. The employee, payroll, human resources, and general public (perhaps accessing the system through the public-facing portion of their website) will all have different levels of access to information. You probably have the following lattice of access.

          employee
       /           \
      /             \
  payroll        human resources
     \              /
      \            /
          public

These security levels would make sense because public would have the least access (public bio perhaps), payroll would need access to things like your salary, human resources would need access to a record of disciplinary action, and you'd have access to all the information as you probably inputted most of it. This is one of many possible structures a company might have. I'd argue access to employee information is definitely a matter of privacy.

That said you're right that there is a dynamic nature of this discussion. What happens if access depends on my geographic location? That information will be stored in a database. This information is dynamic, but you can still use static checking. It'd look something like the following:

  location := getLocation(usedID);
  match location with
  | UK -> ...
  | US -> ...

Now, you don't know what location you have, but once you pattern match on it, you can check `...`s according to the correct level statically because you know that you can never execute that code if the location was elsewhere. So we use dynamic checks to reveal static information.

The big type-theoretic idea here is "existential types" that packs data and not reveal information until it is unpacked.

Hope that was helpful. That was a great great question.

The goal is the same but the approach is different. This is entirely compile time and it covers all executions of the program, whereas taint analysis done at runtime and consider only some executions.

Also taint analysis typically doesn't track implicit flows described in the post, but detects the explicit ones.

Let's say we have `a, b, d : 0` and `c : 999`. Then `a := b :>> c := d` according to your rule is well-typed and has a security level `999`.

Now let's say I have a conditional expression `private : 999`.

The following program typechecks according to the rest of the restrictions. In particular, `999` from `private` is less than or equal to the `999` from the sequenced command.

  ITE private $
    a := b :>>
    c := d

But we just leaked data because if the value of `a` (which we can observe) is not `b`, then we know that `private` was 0 (aka. false). This should never happen because `a` is public and `private` is private.

The intuition here is that the lower the security level a command has the more public the conditional has to be. Otherwise, private data would *influence* public data which we can then observe to deduce something about the private data.

> it seems like you could leak info by just assigning two variables, where one is always public.

I didn't quite follow this bit. But if you elaborate, I'm happy to discuss.

My bad, sorry =)

The share from this story is that we can enforce privacy just as we enforce more traditional types at no runtime cost. It scales because it is compositional and compiler can guide us through programs that won't leak data.

A more niche outcome is that Haskell's traditional type system is rich enough to encode this privacy enforcing type system.

I think if you just ignore the syntax, you can still gain a good intuition about how data might leak in subtle ways and what is sufficient to prevent it.

That is a different notion of typing. The type systems you are referring to (which is how they are commonly understood) classify data according to the operations they support. In this post, types classify privacy. These two notions are orthogonal and can be combined if needed. There are many many more notions of typing out there achieving wildly different goals.

Wouldn't that require the programmer to be adversarial?

Since all type systems have escape hatches, I don't think they would be resilient at all in adversarial settings. This is more geared towards detecting accidental and _subtle_ data leakage.

The point is often you don't need to. If you use Google docs, the chances are you will be editing it disjointly most of the time and occasionally you'll edit the same bit of the document. Then you don't really care if what comes out is a meaningful sentence, but that all parties involved (regardless in which order they see the operations) see the same version of the document so that they can fix it. That's what CRDTs buy you.

Without them, you have to use either explicit synchronisation which is a bad idea if you want local-first software (doesn't work offline, needs to be done even when editing disjoint bits of the file, etc.) or something like CRDTs. Now there is a great paper by Victor Gomes, Martin Kleppmann, and Dominic Mulligan that proves (in a proof assistant!) that pretty much all other alternatives that do not use strong consistency is flawed in edge cases.

As for triviality of the operations, I know for a fact that Martin Kleppmann has a paper in the works that show (and prove) how to do tree move efficiently as a CRDT. That means you can basically do arbitrary edits on JSON. Hopefully, that should clear up any confusion about for which applications it might be useful.

That doesn't help at all because although Datalog is a syntactic fragment, its dynamic semantics are very different, so the operations defined in Prolog standard are suggestive at best and completely nonsensical at worst.

For example, the program `p(X) :- p(X)` with query `?- p(X)` is an infinite loop in Prolog but in Datalog it terminates trivially and is equal to the empty set of facts for `p` in the absence any other facts.

I think it's more cultural than anything else. SQL, despite being declarative itself, has a more imperative feel to it for some people (recursion being at the fringes of its standard) and people seem to believe more declarative means slower and more difficult to comprehend. The former is true only due to the implementation effort that went into SQL engines and the latter is plain false.

It probably doesn't help that the standard presentation of Datalog looks very much like Prolog, which most people think is an esoteric and failed programming language.

As for its limitations, it's disciplined in a number of ways, but those are features rather than shortcomings. So you can see in the post that it employs syntactic restrictions to ensure domain independence, it doesn't allow function symbols to have termination. It requires predicates that are not purely logical (extralogical) to satisfy certain conditions for safe execution. These make sure that your queries are well-behaved even before you start running the query. There is research on relaxing these restrictions (cough my work cough) without compromising on the nice properties that come along with it.

The nice thing is of course that if you want to do the same for SQL you start with pandora's box open and try to contain the chaos inside again, while with Datalog you're carefully trying to make the best out of it without unleashing madness. The latter is a much nicer foundation.