Synergy in Scheme

This partly refutes my following comments.

The Safe

Here is the simplest addition to Scheme I know that provides efficient synergy. I posit a new primitive type, safe, and three new widely available primitive functions, make-safe, extract and safe?. The safe is like the cons cell except there is neither car nor cdr for it. make-safe is a new two argument primitive procedure like cons except it produces a safe instead of a cons cell. (make-safe brand value) returns a new safe and only a holder of brand can extract the value. extract takes two arguments—safe? takes one or two. The following is true regardless of the values of a, b and c:

(and (eq? (extract a (make-safe a b)) b)
     (or (eq? a b) (not (extract b (make-safe a c))))
     (or (safe? a) (not (extract a b)))
     (safe? (make-safe a b))
     (safe? (make-safe a b) a)
     (boolean? (safe? a))
     (boolean? (safe? a b))
     (eq? (eq? a b) (safe? (make-safe a c) b)))

The holder of a brand is able to extract the content from any safe with that brand that he finds. For now (extract a b) yields false if b is not a safe. REPLs for Scheme have various ways of reporting domain errors for primitives. In practice users of extract can use the more discriminating safe? if someone should store #f in a safe. The only runtime cost is when this is the case.

The garbage collector needs to learn about the safe. If it encounters a safe the value therein should not be preserved unless the corresponding brand is found elsewhere. This implies a list of deferred decisions about values found in safes.

I discuss another pattern, called the sealer-unsealer, here. Both these proposed primitives support the other synergy patterns and each other efficiently as well.

The following defines make-safe, extract and safe? in terms of new-seal and eq?.

(define ctool (let ((s (new-seal)))
  (let ((seal (car s)) (unseal (cadr s)) (sealed? (caddr s)))
    (let ((make-safe (lambda (a b) (seal (cons a b))))
          (extract (lambda (b p) (and (sealed? p) (let ((c (unseal p)))
             (and (eq? (car c) b) (cdr c))))))
          (safe? (lambda (a . l) (and (sealed? a) (or (null? l)
             (and (pair? l) (null? (cdr l)) (eq? (car l) (car (unseal a)))))))))
    (list make-safe extract safe?)))))
(define make-safe (car ctool))
(define extract (cadr ctool))
(define safe? (caddr ctool))

The following defines eq? in terms of make-safe and extract:

(define (eq? a b) (extract b (make-safe a #t)))

We have now the following set of reductions:

make-safe, extract and safe? ⇛ eq?
eq? ⇛ new-seal
new-seal and eq? ⇛ make-safe, extract and safe?

The following defines new-seal in terms of make-safe, extract and safe?:

(define (new-seal) (let ((S (cons '() '()))) (list
   (lambda (rep) (make-safe S rep)) ; seal
   (lambda (abs) (or (extract S abs) (if (safe? abs S) #f
       (error "invalid argument" abs)))) ; unseal
   (lambda (x) (safe? x S))))) ; => (seal unseal sealed?)

On 2012 Nov 3 Darius Bacon noted that a previous proposal, without safe?, could not seal the value #f. That is now fixed, but with a bit of extra complexity. On 2014 May 7, Darius noted that my derivation of extract relied on eq?; the derivations are not cyclic. Perhaps the safe primitives are stronger in that sense than the sealer. Some think that a language should not have eq? and they might prefer the sealer for that reason.

Safe vs. Sealer

These primitive sets are of nearly equivalent complexity. Both are presumably easy to implement. Here are the differences I see:

The sealer has been widely discussed. The safe appeared as the domain’s brand in Keykos.
The safe apparatus must expend some uniquely generated object, such as a cons cell, to brand a collection of safes. Perhaps the sealer need not, but it might then need extra logic to recycle the required internal IDs.
make-sealer produces a three values that are of sorts unprecedented in Scheme. Each of these is replicated for users, unlike cons which is shared. I see absolutely no problem with this, but it will confuse a few.
I think you can build a weak map from the safe but not the sealer.

No New Primitive Needed?

Not quite. I add this in 2012, Jan.

The following would seem, at first, to be a slight modification and simplification to the safe, which is trivially implemented in current Scheme!

(define (make-safe a b) (lambda (x) (and (eq? x a) b)))

The modified Guttag definition is:
for arbitrary Scheme values a, b and x:

(let ((s (make-safe a b))) (and (eq? (s a) b) (or (not (s x)) (eq? a x)))) => #t

There seems to be an unsurmountable problem! How does the legitimate holder of the brand know that a value of uncertain provenance is confined? Perhaps it is instead (lambda (x) (set! y x)) where y is some variable in scope of the perpetrator who is attempting to open thereby safes not meant for him.

A Scheme value is a pair of behavior and state. If the behavior could be ascertained by the holder this problem would be solved. That breaks other security properties however. If it could be ascertained that the behavior was specifically “(lambda (x) (and (eq? x _) _))” then that too would solve the problem. Even that is dangerous.

Confusion

The long and expression above is always true which captures most of the semantics of the new primitives. I think that it does not capture the fact that (safe? x) yields #f if x is not a safe. Furthermore the implementation of safe? via seal-unseal has difficulty in implementing this feature of safe?.