259: Tagged procedures with type safety 259: Tagged procedures with type safetyby Daphne Preston-Kendal
This SRFI is currently in draft status. Here is an explanation of each status that a SRFI can hold. To provide input on this SRFI, please send email to srfi-259@nospamsrfi.schemers.org. To subscribe to the list, follow these instructions. You can access previous messages via the mailing list archive.
Tagged procedures are procedures with boxes attached, which can be used to create applicable records and other abstractions. This SRFI proposes a variant with the notion of a tagging protocol, analogous to a record type definition, for ensuring encapsulation and security for tagged procedures.
None known.
The rationale of tagged procedures is well explained by the original SRFI 229. That SRFI has a flaw, though, hiding in plain sight within this sentence in its rationale:
In fact, in the context of SRFI 229, one shouldn’t think of procedures falling in just two classes, untagged and tagged ones (note that all procedures may be implementable as tagged ones), but falling into infinitely many classes, one for each type of its tag.
Since there are infinitely many types of tagged procedures, tagged procedures should themselves be typed. A system of tagged procedures without this feature is somewhat like a system of records built on Scheme vectors and pairs rather than true record types.
Specifically, the value in the tag box of a tagged procedure may be intended, by the usual consumers of the tagged procedure, to imply something about the behaviour of the procedure. But this contract can be broken by mischievous code which takes the tag value from one procedure and attaches it to another procedure which doesn’t have the expected behaviour. In a context where procedure tags might be used for security purposes, that procedure might in fact have some very unwanted nefarious behaviour.
Creating a system of typed tagged procedures, where only the holder of the correct accessor and constructor procedures can directly create tagged procedures of a certain type, makes tagged procedures type safe and suitable for use in security-oriented protocols.
(define-procedure-tag constructor name predicate name accessor name) — syntaxSyntax: The subforms are all identifiers. Define-procedure-tag is a definition form.
Semantics: Define-procedure-tag binds the identifiers constructor name, predicate name, and accessor name to three procedures for a newly-created tagging protocol.
The constructor name is bound to a constructor procedure of two arguments, tag and proc. Proc must be a procedure, referred to as the underlying procedure. When invoked, the constructor procedure returns a new procedure object which has identical arity and behaviour as the underlying procedure, but is tagged in the new tagging protocol with the object TAG. If the underlying procedure is already a tagged procedure in some protocol or protocols, the new tag is added in the newly-returned procedure to the existing ones, with the given tag; if one of those protocols is the created tagging protocol, the tag value for this protocol is effectively replaced with the new tag value.
The procedure object returned from the constructor procedure has a fresh location tag and is distinct from all existing procedures in the sense of the eqv?, eq?, and equal? procedures.
The predicate name is bound to a predicate procedure of one argument. When this procedure is invoked, it returns #t if its argument is a procedure object that was created by a call to the constructor procedure, or #f otherwise.
The accessor name is bound to an accessor procedure of one argument. Its argument is a procedure object created by a call to the constructor procedure, otherwise an assertion violation is signalled. The accessor procedure returns the value of the tag which was provided when the constructor procedure was called.
Define-procedure-tag is generative: every evaluation causes the creation of a new procedure tagging protocol, and the constructor, predicate, and accessor procedures created do not operate on tagged procedures with the protocol from previous or future evaluations of the same define-procedure-tag form.
Procedure tagging protocols do not create a disjoint type: the procedure? predicate answers #t on tagged procedures.
The following sample implementation is in terms of SRFI 229. Of course, if user programs are given direct access to SRFI 229, the type safety can be broken.
(define-library (srfi 259)
(export define-procedure-tag)
(import (scheme base)
(srfi 229))
(begin
(define-record-type Tag
(make-tag vals)
tag?
(vals tag-vals))
(define-syntax define-procedure-tag
(syntax-rules ()
((_ constructor predicate accessor)
(begin
(define key (cons 'constructor '()))
(define (constructor tag underlying-proc)
(if (and (procedure/tag? underlying-proc)
(tag? (procedure-tag underlying-proc)))
(lambda/tag (make-tag
(cons (cons key tag)
(tag-vals
(procedure-tag underlying-proc))))
args
(apply underlying-proc args))
(lambda/tag (make-tag (cons (cons key tag) '()))
args
(apply underlying-proc args))))
(define (predicate obj)
(and (procedure/tag? obj)
(tag? (procedure-tag obj))
(not (not (assq key (tag-vals (procedure-tag obj)))))))
(define (accessor proc)
(cond ((assq key (tag-vals (procedure-tag proc)))
=> cdr)
(else (error "not tagged in this protocol" proc))))))))))The following code implements the core of the T object system (also known as the ‘operations’, ‘YASOS’, or ‘Scheming with Objects’ system). The exports are object, object?, operation, operation?
(define-procedure-tag make-object object? object-vtable)
(define-syntax object
(syntax-rules ()
((_ proc-expr ((operation . formals) body_0 body_1 ...) ...)
(letrec*
((proc (cond (proc-expr)
(else (lambda ignored
(assertion-violation #f
"object not callable")))))
(obj
(make-object
(list
(cons operation
(lambda formals body_0 body_1 ...)) ...)
proc)))
obj))))
(define (find-method obj op)
(cond ((assv op (object-vtable obj)) => cdr)
(else #f)))
(define operation?
(object (lambda (x) #f)
((operation? self) #t)))
(define-syntax operation
(syntax-rules ()
((_ default-expr ...)
(letrec*
((default default-expr)
(op
(object (lambda (obj . args)
(cond ((and (object? obj)
(find-method obj op))
=> (lambda (method)
(apply method obj args)))
(else (apply default obj args))))
((operation . formals) body_0 body_1 ...) ...)))
op))))Thanks to Marc Nieper-Wißkirchen for the original SRFI 229 and for identifying the flaw in it to me.
© 2025 Daphne Preston-Kendal.
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice (including the next paragraph) shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.