Scheme:call/ccと副作用

Scheme:call/ccと副作用

c.l.sで興味深い議論が進行していたのでメモ。

purely functional Lisp + call/cc = ?

発端は、Nils M Holmの

「Purely functionalなマイLispにcall/ccをつけてみたよ」

という投稿。

それに対し、Schemeの大御所達から

「call/ccは、副作用を生じるよ」

と突っ込みが入る。

言い替えれば、「set!などの明示的な副作用オペレータを一切持たない purely functionalなLispに、call/ccを導入すると、それはもはや purely functionalではなくなる」ということ。

実例

これは簡単な例によって示すことができる。szgygによる例:

(let ((f (lambda (x)
           (call/cc (lambda (k) k)))))
  (cons (f 0) (f 0)))

(f 0)の2回の呼び出しは、同じ関数に同じ引数を渡しているにもかかわらず、 戻り値が異なる。

Al Petrofskyによる例。「purely functional Schemeの特性のひとつは、 関数引数の評価順序がどうであろうとそれが外部から検出できないことだ。 しかし次のコードは関数引数の評価順序を検出できる。」

(call/cc (lambda (k) (0 (k 1) (k 2))))  =>  maybe 1, maybe 2

Anton van Straatenによる、インタラクティブに副作用を確認できる例:

(define foo
  (let ((old-k (call/cc (lambda (k) (cons k #f)))))
    (let ((k (if (pair? old-k)
                 (call/cc (lambda (k) ((car old-k) k)))
                 (call/cc (lambda (k) k))))
          (flag '(flag)))
      (lambda (x)
        (cond
          ((procedure? k) (k x))
          ((eq? k flag) (* x 2))
          (else (if (eq? x 42) (old-k flag) k)))))))

Here's a transcript of its behavior in Scheme:

> (foo 23)
> (foo 5) 
23
> (foo 6) 
23
> (foo 42)
> (foo 5) 
10
> (foo 6)
12

Al Petrofskyによる別の例。fが同じ引数 (call/cc) を受け取っているのに 異なる整数値を返す (実際には、fは4回帰っている。(1)手続きcall/cc (2)数値1 (3)手続きcall/cc (4)数値2。

(let ((f (lambda (x) (x x))))
  (let ((result1 (f call/cc)))
    (if (procedure? result1) (result1 1))
        (let ((result2 (f call/cc)))
          (if (procedure? result2) (result2 2))
              (list result1 result2))))
  => (1 2)

意味

「call/ccが副作用を行うオペレーションである」というのは何故か、 と考え出すと色々深い。

Matthias Blumeがなかなかうまい要約を示した。

CPS変換はプログラムのグローバルな書き換えだ。 グローバルな書き換えを行えば、どんな副作用だって消すことができる。 (ある意味、これが「副作用」の「定義」であるとも考えられる。 すなわち、ローカルではなくグローバルでないと説明できないもの、ってことだ)

Anton van Straatenが参照透明性の観点から補足する。

(call/cc (lambda (k) (cons (k 1) (k 2))))

このプログラムは、(k 1) や (k 2) を値に置換することでは計算できない。 もしcall/ccが「副作用」を起こしていないとしたら、ここで参照透明性が 崩れることを何と説明する?

私自身は両手をあげて「これを副作用と呼ぼう」と言うことしかできないが、 もっとうまい理論的な説明があるなら知りたい。

関連スレッド

Tags: 継続, call/cc


Last modified : 2012/02/07 08:23:57 UTC