This note is inspired by A Security Kernel Based on the Lambda-Calculus by Jonathan Rees. That paper provides the conceptual prerequisites for this note. This idea also relates to Keykos sensory keys. This idea is sometimes called “transitive read-only”. The Language Forsythe has a “Source” construct which is related to these ideas.

Proposal for Scheme and Sensory Data Access

Associated with every pair is a seepair. If x is a pair then (see x) is the corresponding seepair.
If x is a pair then (car (see x)) = (see (car x)), (cdr (see x)) = (see (cdr x)), and if x is a seepair then neither (set-car! x) nor (set-cdr! x) have an effect and should signal an error.
see neither allocates storage nor makes a copy. (see x) refers to the same locations as x but conveys no ability to change what those locations hold. Those locations may still be modified thru x. The pair and the seepair occupy the same storage.
(let* ((x '(3 . 4))(y (see x))) (set-car! x 42) (car y)) => 42.

Associated with every vector is a seevec. If v is a vector then (see v) is the corresponding seevec. (vector-ref (see v) k) = (see (vector-ref v k)) and (vector-length (see v)) = (vector-length v). (vector-set! (see v) n x) and (vector-fill! (see v) x) have no effect. (vector->list (see v)) = (see (vector->list v)). If b is a list then (list->vector (see b)) = (see (list->vector b)).

For every string there is a corresponding seestring. If s is a string then (see s) is the corresponding seestring.
(string-length (see s)) = (string-length s).
(string-ref (see s) k) = (string-ref s k).
(string-set! (see s) k c) has no effect and should signal an error.
If x is one of string=?, string-ci=?, string<?, string>?, string<=?, string>=?, string-ci<?, string-ci>?, sring-ci<=?, string-ci>=?
and strx1 is either (see str1) or str1
and strx2 is either (see str2) or str2
then (x strx1 strx2) = (x str1 str2).
(substring (see str) k l) = (substring str k l).
(read-only str) = (see str).

For all x, (see (see x)) = (see x).

I think that (pair? (see x)) = (pair? x), (vector? (see x)) = (vector? x) and (string? (see x)) = (string? x). This is for further study.

We define see? thus: (see? x) = (eqv? x (see x)). This predicate corresponds to “sensory” in Keykos.
Literals produce sensory values but primitive constructors don’t:
(see? '(0 . 0)) but not (see? (cons 0 0)).
(see? #(3 5 7)) but not (see? (vector 3 1)).
(see? "gx") but not (see? (string #\g #\x)).
It is no longer necessary as an additional language rule to declare it an error to modify the value of a literal.

If (or (procedure? x) (port? x)) then (eq? (see x) '()). If (or (boolean? x) (symbol? x) (char? x) (number? x)) then (eq? x (see x)).
(see '()) = '().

Associated with each vector is a rovec of the same length and members. If v is a vector then (read-only v) is the corresponding rovec.
(length (read-only v)) = (length v)
(vector-ref (read-only v) k) = (vector-ref v k), unlike (see v)!
(vector-set! (read-only v) k x) and (vector-fill! (read-only v) x) have no effect and may signal an error.
Read-only could also be logically applied to pairs but we don’t need that. Do we have “If (eq? x y) then (eqv? x y)”? Not for NaN.

Phrases such as “fresh locations holding undefined values” in R5RS must be somehow qualified to insure that those values are not my secrets—even that they are statistically independent of my secrets. They must also not convey the ability to step on my secrets. In the jargon of denotational semantics, bottom must be relativized. If the jargon of OS’es your bug must not corrupt my world. We must make some statements about erroneous programs.

Of course there are really pointers underneath.

The introduction of the environment seems to miss the point that the same occurrence of an expression is evaluated in different environments at different times. I don’t see a clear stance as to whether environments are mutable. Being extendable is less dangerous than being mutable. The text in eval

Integrate with this. 

(define fc (let* (
   (factory-seal (new-seal))
   (fac-seal (car factory-seal))
   (fac-unseal (cadr factory-seal)))

(lambda (n)
(let* (
  (seal (new-seal))
  (sealer (car seal))
  (unsealer (cadr seal))
  (components (vector n '())))
 (lambda args (case n 
   ((1) ; Install a sensory component.
     (vector-set! components (cadr args) (see (caddr args))))
   ((2) ; Install another requestor’s key
     (if (fac-unseal (caddr args))
       (vector-set! components (cadr args) (caddr args))))
   ((3) ; Seal factory and return requestor’s key.
     (let ((requestor (lambda args
         (eval (vector-ref components 0) 
     
     
     (fac-seal requestor) requestor)

A Manner of Speaking

The above fiction of a sensory object hovering about the mutable object may seem obscure. To some it would more natural to speak of read-only capabilities. I don’t intend to argue here about which is better. I tried to follow Scheme’s descriptive style and general ontological framework. Just now (2010) I think I prefer Rees’ Scheme. However I think that my scheme is polymorphic in a fundamental way. A Scheme function to run down a list need not know that it is an immutable list. In the Rees Scheme that function must know to use cell-ref.

Still there remains a possible advantage to my scheme. Since car can operate on either a pair or seepair, readers of a list need not discriminate between the two and a list builder can construct mutable lists, and indeed looped lists which behave as ordinary lists to the reader. In Rees’ Scheme looped lists can be constructed but extra logic is required by the reader. I do not now know how to combine the advantages of the two schemes. Another advantage of my scheme is that I can grant read-only access to a mutable structure. I retain the ability to mutate the structure even as you navigate it. This is dangerous, but fundamental.

I think that seeprocs are also feasible. The environment of the procedure would be weakened (made sensory). The cleanliness of Scheme semantics makes this feasible. I am not sure of the ramifications on implementations but I would suppose that the trip up the dynamic chain of environments would include a read-only check at each step. If a bit were allocated within the address of environments, then this extra cost would be about one very efficient machine op (a register or) per static nest depth per variable reference.