Formal comment #36 (defect)

Ambiguous call/cc-behaviour of list operations
Reported by:	Andre van Tonder

Component:	miscellaneous
Version:	5.91

Pages : p.45 (pairs and lists) and also pp. 63-65 (list utilities) 
Summary

Some list operations are ambiguous in the presence of call/cc. They
may easily be unambiguously specified, for example in the way proposed
below. Description

Various list procedures including map, fold-right, reverse, etc. are
not currently specified unambiguously in the presence of call/cc.

One of the first difficult bugs I encoutered in a Scheme program I
wrote was the following (see e.g. Sitaram's book for amb and
amb-collect = bag-of):

  (define (f x)
    (amb 0 1))

  (amb-collect (map f '(0 0)))  ==> ((0 1) (0 1) (1 1) (1 1))  !?

This surprising result could be traced to the following imperative
implementation of map - which is r6rs-conformant as far as I can tell
- in the host implementation:

  (define (map f lst)
    (if (null? lst)
        '()
        (let ((result (list (f (car lst)))))
          (let loop ((pair result)
                     (tail (cdr lst)))
            (if (pair? tail)
                (let ((pair* (list (f (car tail)))))
                  (set-cdr! pair pair*)
                  (loop pair*
                        (cdr tail))))
            result))))

whereas the natural functional implementation would give the correct
result ((0 1) (0 1) (1 0) (1 1)).

Nothing in the wording of the r6rs document seems to exclude the
imperative implementation. I know of at least one major implementation
whose map used to behave this way. So the behaviour of map, reverse,
fold-right, etc. is potentially ambiguous.

Here is another test I found not relying on amb, due originally to
Matthias Radestock, I believe:

  (let ((result
         (let ()
           (define executed-k #f)
           (define cont #f)
           (define res1 #f)
           (define res2 #f)
           (set! res1 (map (lambda (x)
                             (if (= x 0)
                                 (call/cc (lambda (k) (set! cont k) 0))
                                 0))
                           '(1 0 2)))
           (if (not executed-k)
               (begin (set! executed-k #t)
                      (set! res2 res1)
                      (cont 1)))
           res2)))
    (if (equal? result '(0 0 0))
        (display "Map is call/cc safe, but probably not imperative.")
        (display "Map is not call/cc safe, but probably imperative."))
    (newline))

Proposal

Consider fully specifying the list operations by inlining a reference
implementation for each as part of the descriptive text. This should
be easy, since these reference specifications are all very short.

I do not know if there is any reliable way of fixing the ambiguity via
prose.

Andre

RESPONSE:

Some ambiguity is desired.  Prose specifications often contain
too much ambiguity, while specifications as code often contain
too little.  This is a well-known problem with specifications
in general.

It wouldn't hurt to have less ambiguous specifications, but
specifications as code aren't going to be very simple given
the complexity of requirements introduced by the draft R6RS.

The map procedure, for example, could be required to behave
as though defined by

(define (map f x . rest)

  (define (check-arguments)
    (if (not (and (list? x)
                  (let ((n (length x)))
                    (forall (lambda (y)
                              (and (list? y) (= n (length y))))
                            rest))))
        (apply contract-violation 'map
                                  "illegal list arguments"
                                  x rest)))

  (define (map1 f x)
    (if (pair? x)
	(cons (f (car x)) (map1 f (cdr x)))
	'()))

  (define (mapn f lists)
    (if (pair? (car lists))
	(cons (apply f (map1 car lists))
	      (mapn f (map1 cdr lists)))
	'()))

  (check-arguments)
  (mapn f (cons x rest)))

The above specification as code avoids specifying the dynamic
order in which f is applied to the elements of the lists, but
does not allow all of the behaviors that the draft R6RS was
intended to allow.  For example, the above specification as
code would rule out copying of all list arguments on entry,
which is in some ways a more desirable implementation than
the one given above.

If the first argument to map were forbidden to have side
effects, then the above specification as code would work
better.  This is an example of how prose and code can work
together to provide less ambiguous specifications, which
would be an improvement over the draft R6RS.  Doing so in
a consistent manner involves a great deal of careful work
and caution to avoid overspecification.

The next draft of the report will address this issue in a manner
consistent with our resolution of formal comment #87.  In particular,
we may acknowledge and embrace a certain amount of ambiguity to
avoid unnecessary implementation constraints and also to avoid
making guarantees about exceptions that will be raised, thereby
converting programs that we all might agree are invalid into ones
that are valid because they are always guaranteed to
raise exceptions with certain conditions.