On A Study of Capability-Based Effect Systems

It is still uncommon today to move concepts and solutions between the domains of: The map for this bridge is to consider the ‘syntax of the OS’ to be binary machine language; the OS executes binary programs. The file system of the conventional OS serves as a global scope from the perspective of language. There is no global scope for a capability OS. For the OS there are commonly some sort of interprocess messages which serve a rôle of function call in the language realm.

The paper confused me because it limits “capability” to those functions that can exfiltrate their arguments as in (lambda (x) (print x)). Perhaps that is the meaning of the phrase “capability-based effect systems”. I would not object to the term “effect-capability” here. Seeing Scheme, in capability terms, even cdr is a capability although not one that steals your data.

In this Scheme example:

(let ((Z (lambda () (let ((x 0)) (cons (lambda () (set! x (+ x 1))) (lambda () x))))))
  (let* ((p (Z)) (inc (car p)) (r (cdr p))) (inc) (inc) (inc) (r)))
This whole expression yields 3 but the scope of the counter x, is within the first line.

In their definition of stoic, Z is a stoic function even though it captures values {0, cons, +} none of which are larcenous, from an outer scope. Those are the free variables in the body of the definition of Z and not among the parameters. (Most would exclude 0 from this list but I think that “0” denotes just like “x”.)

I don’t recognize the phrase “problem of effect polymorphism” in their abstract. Matt Rice refers me to this paper.
Perhaps the free variables in the body of the definition of a stoic function may include only the parameters and variables bound to other stoic values. That is an easy compile time check. {0, cons, car, +} are all stoic values.
I think that all Haskell values are stoic.

I call Scheme an object based language; for what is the yield of Z but an object? There is a small implementation difference in that the value the Z returns captures the address of x twice. I have not read most of the paper but I wonder if the notice the opportunity of applying “stoic” to functions that return objects. In their “Future Work” section they aspire to objects. Perhaps their work already covers that under the proper interpretation of ‘object’. That pattern provided that main attraction for Keykos factories. The factory pattern excludes:

(let ((Y (let ((x 0)) (lambda () (cons (lambda () (set! x (+ x 1))) (lambda () x))))))
  (let* ((p (Y)) (q (Y)) (inc (car p)) (r (cdr q))) (inc) (inc) (inc) (r)))
Y is not stoic because x is free in the body of Y’s definition. (The body starts at the lambda and this takes some careful wording.) In this example inc and r are from separate invocations of Y and the displayed results, 3, show that they communicate. In the Keykos environment a factory is usually shared broadly between those who need privacy from each other as well as the definer of the .program of the factory. It is vital that two yields of the same factory be isolated from each other. This is not the default case for two objects from the same ‘class’ in C++ or Java.

The factory is not structurally incapable of stealing your secrets, but it is trusted to yield objects that are structurally incapable of stealing your objects, despite obeying untrusted code. Two factories are objects that obey the same trusted program but different factories have different .programs which are not trusted to keep secrets. The factory’s .program is what the yield of a factory obeys.

I quote from the manual

That text occurs under the title ‘The ambiguity of “discreetness”’. I wonder now whether we can tolerate this ambiguity. Perhaps we should use “stoic” as an adjective for the factory. I will not soon modify all of the pages on this site however.

The property ‘deterministic’ of functions is like stoic in that it is established recursively. They are independent properties, however; neither implies the other. See this.


Central modern discussion of factory