call/ccが「副作用」である理由

http://practical-scheme.net/wiliki/wiliki.cgi?Scheme%3acall%2fcc%e3%81%a8%e5%89%af%e4%bd%9c%e7%94%a8
(via http://d.hatena.ne.jp/flappphys/20061119#p2)

おお、これは正確でわかりやすい議論ですね。call/ccが参照透明性を破壊する（ややトリッキーな）実例としては、前にちらっと書いた

> (define x (call-with-current-continuation call-with-current-continuation))
> x
#<system continuation>
> (x 123)
> x
123

も、その筋ではよく知られているようです。元のcomp.lang.schemeの議論をちゃんと読んでいないので既出かもしれませんが。（Schemeではトップレベルのdefine ≒ set!という定義なので正確には微妙ですが、letでも同じような例が作れます。）

また、値制限のないML多相に破壊的代入(reference cell)を導入すると不健全になることは先に触れましたが、value restrictionのないML多相 + callccも同様にunsoundです。（後者はちゃんと説明しないで

破壊的代入やcall-with-current-continuationなど「副作用」のある言語では、上述の型推論は不健全になる。

と軽く流してしまいましたが…）

さらに、Haskell等の「副作用をモナドで表す」話の元となった、Moggiのcomputational lambda-calculusでも、状態を表すstate monad等と同様に、continuation monadがあります。これについてはディープな研究があって、（ちょっと不正確な要約かもしれませんが）Filinskiの博士論文において、任意の「副作用」はcontinuation monadと一個のreference cellで表せることが示されていたりします。

もっとも、これらはcall/ccが副作用である「状況証拠」にすぎず、Shiroさんもおっしゃっているように、結局はMatthias Blumeの

Notice that CPS conversion is a /global/ rewrite of the program.　　/Any/ side effect can be eliminated using a global rewrite. (In some　sense you can take this as a "definition" of "side effects": something　that cannot be explained locally but only globally.)

につきるかもしれません。ちなみに、このMatthias Blumeさんは、京大におられたり、トヨタがシカゴ大学の近傍（内部？）に設立した研究機関におられたり、日本とつながりの深い方のようです。（実はあまりお会いして話したことはないのですが）

P.S. 実は、value restrictionのないML多相の下では、（call/ccがなくても）CPS変換は型を保存しないことが証明されています。つまり、CPS変換すると、well-typedなプログラムがwell-typedでなくなってしまう（ことがある）ということです。もちろん、simply typed lambda-calculusやpolymorphic lambda-calculus (System F)ならばOKですが、後者では型推論が決定不能問題だったりします。このような問題があるので（それだけが理由ではありませんが）、型を消去しないで保存するようなコンパイラでは、ソース言語はML多相でも、中間言語はSystem Fにする、というアプローチを採ることが多いようです。