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

[didibus]

Thanks for taking time to answer, if you can have something more akin to permission categories, that makes it more interesting to me.

By dynamic, in your example, I'm meaning that for example as an employee I shouldn't have access to other employees data, only my own. I don't see how that can be handled statically.

Also, in the code for your lattice example, I guess you'd have a different page for each one? So like one page for human-resource and the variables in the code for that page would be of security-level human-resource. So in that way I get it, you can't accidentally for example on the public profile page add a payroll level information, because assigning from the payroll to the public page would error. But how do you now control access to which page the user has access too? Maybe for this you still need a dynamic permission system on top? And the compile checks only prevent programmer accidentally showing the wrong data on the wrong page?

Lastly, I still don't know if I buy into "levels". From my experience in enterprise systems, requirements always end up that there's no real hierarchy, just various overlapping sets. For example, it's very likely that human-resource would need to see data which the employee shouldn't see, like performance reviews, HR violations about the employee, compensation targets, etc. Similarly I can imagine payroll needing to see some company related financial with regards to the employee pay which the employee shouldn't have access too as well.

That's where I feel levels wouldn't meet requirements, since you rarely have scenarios where one category is a strict superset of another.

I can even imagine this causing leaks, as a programmer might get confused and think: "employee is the highest level, so I guess all those fields I added to the HR page should also go on employee and the assignment succeeds since employee is highest level of privacy, perfect I can leak no data". And now you've leaked private internal company data to the employee.

So here I think what be cool is if I could instead say that some function returns a value of security [payroll, employee] and another function returns a value of [payroll], while yet another returns [employee]. And now a [payroll, employee] can be assigned to a [payroll] or a [employee] or a [payroll, employee], but you can't assign a [payroll] to a [payroll, employee].