Monadic Library for Eio Capabilities?

[kantian]

@bluddy

think all of this shows that this is a layer of complexity we didn’t sign up for.

Indeed, Eio is far more than just a library for concurrency/parallelism. Furthermore, even if I find the idea of capabilities very interesting (that’s a notion and a conception of security I learned from Eio), it’s not the only way to solve safety problem. For instance, @dinosaure who writes unikernel can do this by restricting the number of system call allowed by his code, and maybe that’s why he wrote his own effect based scheduler.

@bluddy

OCaml’s type system isn’t powerful enough to manage this additional baggage without bogging users down in complexity.

OCaml type system can do a lot, but it’s not sure any user wants to pay that price just to have more safety control on their code. For instance, IIRC @c-cube wrote a simpler version of access control with [R|W] phantom type on bytes but I guess he stopped using it. And he also wrote his own effect-based scheduler.

---

The rest of this comment is more for people interested by philosophy of law and how it relates to object-capabilities system. I mostly thinking out loud since I only start reading about capabilities last week but I’ve been reading Kant’s philosophy for more than 25 years.

Since capabilities system deal with the right some code have regarding some resources, It must have some analogy with how the law works among human beings, and indeed it has. First of all, when I said that Curry-Howard was a particular case of a more general principle (not only use to study the analogy between computation and mathematical proof) I was serious. Let’s look at what Kant said about the formal structure of a State (his philosophy of law can be seen as a typing theory of roman law):

@Kant

Every State contains in itself three Powers, the universal united Will of the People being thus personified in a political triad. These are the Legislative Power, the Executive Power, and the Judiciary Power.—1. The Legislative Power of the Sovereignty in the State, is embodied in the person of the Lawgiver; 2. the Executive Power is embodied in the person of the Ruler who administers the Law; and 3. the Judiciary Power, embodied in the person of the Judge, is the function of assigning every one what is his own, according to the Law (Potestas legislatoria, rectoria et judiciaria). These three Powers may be compared to the three propositions in a practical Syllogism:—the Major as the sumption laying down the universal Law of a Will, the Minor presenting the command applicable to an action according to the Law as the principle of the subsumption, and the Conclusion containing the Sentence or judgment of Right in the particular case under consideration.

Kant, Philosophy of law.

In other words, a State is formally structure like an Aristotelian syllogism (this is due to the formal structure of human mind: reason, understanding and the faculty of judgment, structure that we project in the constitution of our States).

• the law is the major (legislative power)
• the case at hand is the minor (executive power)
• the sentence is the conclusion (judiciary power)

That’s exactly what we got with a capability:

• the authority is the major
• the resource is the minor
• the capability is the conclusion

and that’s what I explained when I draw the correspondence between type class/trait system and Aristotelian syllogistic. The purpose of the authority is to rule out some uses of the resource, and the purpose of the system is to enforced the law. It can do it absolutely a priori if it is encoded in the static type system (a world with precogs à la Minority Report, system that will be fundamentally despotic if applied to human beings).

For the record, Kant also used this analogy in his famous Perpetual Peace to describe the distinction between a representative and a despotic constitution.

@Kant

Every form of Government, in fact, which is not representative, is properly a spurious form of Government or not a form of Government at all; because the Lawgiver in one and the same person, may, at the same time, be the executive administrator of his own Will.

and in the french version I have, there is this additional remark in parentheses:

@Kant

(de même que dans un syllogisme l’universel de la majeure ne peut être en même temps dans la mineure la subsomption du particulier sous l’universel)

(just as in a syllogism the universal of the major cannot be the subsumption of the particular under the universal).

He also made an interesting use of syllogistic in an article about copyright (with a problem about concurrency), but I only know a french version freely accessible; De l’illégitimité de la contrefaçon des livres.