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