[r6rs-discuss] [Formal] proc in hash-table-update! should not mutate hash-table

From: Daniel Villeneuve <daniel_villeneuve>
Date: Sat Feb 24 14:57:30 2007

William D Clinger wrote:
> Daniel Villeneuve wrote:
> > Does the Standard clearly states what's the legal output of
> > these two tests?
>
> <pedantry>
> You are using the definite article "the" incorrectly. (...)
> </pedantry>

I stand corrected.

> Your definition of vector-map seems buggy to me.

But I did not find any wording in R6RS that would forbid
this behavior.

> While I am aware of a related bug in the map procedure
> provided by 6 of the 11 implementations of allegedly
> R5RS Scheme that I used to run your examples, I would
> hope that the draft R6RS would not allow such an
> implementation of any vector-map that might become
> part of a standard library.

What about a constraint worded like this?

  Consider a specific invocation of a given function whose
  behavior is to call at least one of its arguments,
  generically named "callback". The implementation should
  behave as if the given function is implemented in Scheme,
  with each callback invocation being associated to a Scheme
  continuation. Let {c_i} be the (possibly empty) set of
  continuations associated to each of the n>=0 calls to the
  callback function(s). The implementation should guarantee
  that for any two invocations of c_p (0<=p<n) an c_q
  (0<=q<n), no internal state modifications incurred by
  invoking c_p be in effect (or "visible") when invoking c_q.

By "given function", I mean the R6RS functions that should
be covered by the constraint (map, vector-map, list-sort,
...).

The "as if" rule might not be necessary, but I was thinking
about implementations that could provide more efficient
(native) implementations of some library functions, for
which the notion of continuation could be altered. The
constraint above does not preclude an implementation from
using a faster map or vector-map if it can prove that the
callback can't capture its continuation (directly or
indirectly).

I append an hopefully R5RS-compliant example of 3 different
vector-map implementations, used in conjunction with
call-with-current-continuation:
- vector-map-1 is the one from my prior post;
- vector-map-2 is an incomplete attempt at fixing the
  overwriting problem by always allocating a fresh vector;
- vector-map-3 complies with the above constraint.

I think the constraint above could be interpreted as:

  If the internal algorithm used to implement the given
  function needs to store a value returned by a callback,
  that value can only be stored into locations that are
  freshly allocated after the invocation of the callback.

This is stronger than the first formulation, but allows for
much easier proofs.
--
Daniel
(define (vector-copy v)
  (let* ((n (vector-length v))
         (w (make-vector n)))
    (do ((i 0 (+ i 1)))
        ((= i n) w)
      (vector-set! w i (vector-ref v i)))))
(define (vector-map-1 f v)
  (let* ((n (vector-length v))
         (w (make-vector n)))
    (do ((i 0 (+ i 1)))
        ((= i n) w)
      (vector-set! w i (f (vector-ref v i))))))
    
(define (vector-map-2 f v)
  (let* ((n (vector-length v))
         (w (make-vector n)))
    (do ((i 0 (+ i 1)))
        ((= i n) (vector-copy w))
      (vector-set! w i (f (vector-ref v i))))))
(define (vector-map-3 f v)
  (let ((n (vector-length v)))
    (let loop ((i 0) (r '()))
      (if (= i n)
          (list->vector (reverse r))
          (loop (+ i 1) (cons (f (vector-ref v i)) r))))))
(define (test-vector-map vector-map)
  (let ((r (make-vector 4))
        (k1 #f)
        (k2 #f)
        (j 0))
    (define (f x)
      (call-with-current-continuation
       (lambda (kk)
         (if (and (not k1) (= x -1)) (set! k1 kk))
         (if (and (not k2) (= x -2)) (set! k2 kk))
         (* 2 x))))
    (let ((v (vector-map f '#(1 -1 2 -2 3))))
      (cond
       ((= 0 j)
        (vector-set! r j v) ;; v: plain vector-map
        (set! j (+ j 1))
        (k1 1))
       ((= 1 j)
        (vector-set! r j v) ;; v: vector-map restarted at -1
        (set! j (+ j 1))
        (k2 3))
       ((= 2 j)
        (vector-set! r j v) ;; v: vector-map restarted at -2
        (set! j (+ j 1))
        (k1 5))
       (else
        (vector-set! r j v) ;; v: vector-map restarted at -1
        r)))))
(display "testing vector-map-1: ")
(display (test-vector-map vector-map-1))
(newline)
(display "testing vector-map-2: ")
(display (test-vector-map vector-map-2))
(newline)
(display "testing vector-map-3: ")
(display (test-vector-map vector-map-3))
(newline)
;; eof
Received on Sat Feb 24 2007 - 14:56:51 UTC

This archive was generated by hypermail 2.3.0 : Wed Oct 23 2024 - 09:15:01 UTC