[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: New types; also opacity without passkeys [portable R4RS impl]
>--------------------------------------------------------------------------
> Blair's implementation doesn't satisfy axiom 5, because
> (GET-NEW-PREDICATE <type>) returns true on some objects that
> weren't actually created by (GET-NEW-CONSTRUCTOR <type>).
> Below is a transcript from MacScheme; presumably MIT Scheme
> and Scheme 48 give the same result.
>
> >>> (begin (define <type> (MAKE-NEW-TYPE))
> (define U (GET-NEW-CONSTRUCTOR <type>))
> (define P? (GET-NEW-PREDICATE <type>)))
> p?
> >>> (let ((x (U 37)))
> (P? (cons (car x) (cdr x))))
> #t
>--------------------------------------------------------------------------
Well done! I had overlooked that. The following fixes this shortcoming.
The changes are what lies between BEGIN and END. Briefly, the underlying
rep is now sealed inside an opaque procedure (closure) which reveals its
entrusted datum only when given the secret/hidden `*U-TAG*', which cannot
be forged and which is not accessible outside the MAKE-NEW-TYPE closure in
standard R4RS Scheme.
Note that a hash table which holds its elements weakly would be a preferred
way to implement the registry of U-tagged objects, but that is an issue of
run-time efficiency (in both space and time).
As before, the following is portable R4RS Scheme code. (I tested it in both
MIT Scheme and Scheme 48; I do not have ready access to MacScheme.)
Therefore, insofar as this now satisfies axiom 5 (as well as the others), I
(again) claim that your proposal can be implemented in standard R4RS
Scheme. The following code (I claim) is a constructive proof of that.
It does not require any re-definition of standard forms so it need not be
loaded as a module before any others.
;--------------------------------------------------------------------------
(define *universal-selector?* #f) ; Later toggled to #T
(define *U-domain-extended?* #f) ; ditto
(define make-new-type
(let* ((*UID-counter* 0) ; Global counter so each <type> unique
;; Some kernel level data abstractions for U'd data
(*U-tag* (list 'U-tag)) ; Unique object which is never exposed
;;;------
;;; BEGIN
(*U-registry* (list)) ; (Weak EQ? hash table would be better)
(%U-tag (lambda (x)
(let ((opaque-object
(lambda (message)
(if (eq? message *U-tag*)
x ; untag iff given secret *U-tag*
(error "Error: Nice try" message)))))
(set! *U-registry* ; (A weak hash would be better)
(cons opaque-object *U-registry*))
opaque-object)))
(%U-tagged? (lambda (x) ; (A hash table lookup would be better)
(memq x *U-registry*)))
(%U-untag (lambda (U-tagged-obj) (U-tagged-obj *U-tag*))))
;;; END
;;;----
(lambda ()
(set! *UID-counter*
(+ 1 *UID-counter*)) ; Each new <type> gets a unique ID
(letrec ((me? (let ((*state* ; Unique state datum per <type>
*UID-counter*))
(lambda (x) ; unique proc per new type
(and (eq? me? x)
(begin (set! *state* (- *state*))
*state*))))))
(let ((U (lambda (<datum>)
(%U-tag ; (U <object>) yields a tagged...
(lambda (downer) ; ...proc of one arg (for opaque me?)
(cons (me? downer) ; If that one arg is me?
<datum>))))) ; then unveil the <datum> (WIN tagged)
(D (lambda (object)
(if (not (%U-tagged? object))
(if *U-domain-extended?*
object
(error "Error: Cannot D an un-U'd object" object))
(let ((WIN-flag
((%U-untag object) me?))) ; Check U <type> match
;; If D/U match [i.e., WIN-flag = (WIN . <datum>)]
;; (or if unconditionally unveil)
;; then return the unveiled <datum>
(if (or (car WIN-flag)
*universal-selector?*)
(cdr WIN-flag)
(error "Error: D/U mismatch" object))))))
(P? (lambda (object)
(let ((WIN-flag
(and (%U-tagged? object)
((%U-untag object) me?)))) ; Check U <type>
;; If U match, then WIN-flag = (WIN . <datum>)
;; but be sure to return boolean T/F.
(and WIN-flag
(not (not (car WIN-flag)))))))
)
;;
;; A <type> is an opaque procedure to package its
;; constructor/selector/predicate & me?
;;
(lambda (message)
(case message
((U) U)
((D) D)
((P?) P?)
(else
(error "Error: Unrecognized message" message)))))))))
(define (get-new-constructor <type>) (<type> 'U))
(define (get-new-selector <type>) (<type> 'D))
(define (get-new-predicate <type>) (<type> 'P?))
;--------------------------------------------------------------------------
If you are concerned with the disjointness of these new type predicates
(P?) w.r.t. the standard R4RS predicates in Sec.3.4 (as Aubrey Jaffer
seems to be), then, as I outlined in my response to Aubrey earlier, one
could extend the above as follows:
;--------------------------------------------------------------------------
(begin
(define sys:proc? procedure?) ; Globally capture system PROCEDURE?
(define procedure? 'hook ) ; Global hook for opaquely redefining below
(define make-new-type
(let* ((sys:proc? sys:proc?) ; Locally capture system PROC? at def'n time
(*UID-counter* 0) ; Global counter so each <type> unique
.
.
.
(%U-tagged? (lambda (x) ...))
.
.
.
)
(set! procedure? (lambda (x) ; Opaque re-definition of global PROCEDURE?
(and (sys:proc? x)
(not (%U-tagged? x)))))
(lambda ()
.
.
.
)))
)
;--------------------------------------------------------------------------
Again, this is portable R4RS Scheme, although, as you noted, this would now
need to be loaded as a module before any others can capture PROCEDURE?
themselves.