ゲームをしたいですか？
今日、あなたはなりますcallCC。
callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
-- you are here ^^
その機能矢印の左側にあるものはすべて、対戦相手が行った動きです。矢印の右側はゲームの終わりです。勝つためには、対戦相手が提供したピースだけを使用して、右側に一致するものを構築する必要があります。
幸いなことに、あなたはまだ問題についていくつかの発言権を持っています。ここにこの矢印がありますか？
callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
-- this is your opponent ^^
それ自体に矢印が含まれているものを受け取ると、その左側のすべてがあなたが行うことができる動きを表し、右側の部分がそのゲームブランチの終わりを表し、あなたの一部として使用できる別のピースを提供します（うまくいけば）勝利戦略。
先に進む前に、いくつかのことを単純化しましょう。モナド変換子の側面は単に気を散らすものなので、それを破棄します。型変数ごとに明示的な数量詞を追加します。
callCC :: forall a. ((a -> (forall b. Cont b)) -> Cont a) -> Cont a
さて、そのようなタイプが何に相当するかを考えてみforall a. ...てください。そのようなタイプで何かを作成する場合は、どのタイプにも値を提供できると言っていますa。そのようなタイプのものを受け取った場合は、使用する特定のタイプを選択できます。A -> ...これを単形関数のようなタイプと比較してください。このような関数を生成すると、タイプの任意の値の結果を提供する方法を知っていることになりますが、Aこのような関数を受け取ると、使用する特定の値Aを選択できます。これは、と同じ状況のようでforallあり、実際には並列が成り立ちます。したがって、私たちはあなたまたはあなたの対戦相手がタイプforallをプレイするようになる動きを示すものとして扱うことができます、用語ではなく。これを反映するために、私は表記法を乱用し、次のように書きforall a. ...ますa =>。(->)次に、バインドされている型変数の使用の左側に表示される必要があることを除いて、同じように扱うことができます。
また、typeの値を使用して直接実行できるのは、それにCont a適用runContすることだけであることに注意してください。したがって、事前にそれを行い、関連するすべての数量詞をの型に直接埋め込みますcallCC。
callCC :: a => ( (a -> (b => (r1 => (b -> r1) -> r1)))
-> (r2 => (a -> r2) -> r2)
) -> (r3 => (a -> r3) -> r3)
他の関数の矢印と同じように扱うことができるのでforall、物事を並べ替えたり、余分な括弧を削除して、物事を少し整理することができます。callCC特に、それが実際にゲームの終わりではないことに注意してください。関数を提供する必要があります。これは、右端の矢印の役割を果たす別のゲームを提供することを意味します。したがって、それらをマージすることでステップを節約できます。また、型引数を左側にフロートさせて、すべてを1か所にまとめます。
callCC :: a => r3 => (a -> r3)
-> (r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2)
-> r3
だから...私たちの動き。
タイプの何かが必要ですr3。私たちの対戦相手は4つの動きをしましたが、それは私たちが議論として受け取ったものです。一つの動きはを選択r3することです、それで私たちはすでに不利になっています。もう1つの動きはa -> r3、です。つまり、をプレイできればa、対戦相手は咳をして、惰性r3で勝利することができます。残念ながら、対戦相手もプレイaしたので、始めたところに戻ってきました。タイプの何かa、またはタイプの何かを取得するための他の方法が必要になりr3ます。
対戦相手が行った最後の動きはより複雑なので、それを単独で調べます。
r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2
これが彼らが行った動きであることを忘れないでください。つまり、ここで右端の矢印は対戦相手を表し、左の矢印はすべて私たちが実行できる動きのタイプを表しています。この結果は、私たちがプレイできるタイプr2の何かです。r2したがって、明らかに、どちらr3かをプレイするかa、進歩を遂げる必要があります。
再生a：aとして再生する場合は、としてr2再生できます。もう1つの動きはもっと複雑なので、その中に飛び込みます。ida -> r2
b => r1 => a -> (b -> r1) -> r1
私たちを表す右端の矢印に戻ります。今回は、対戦相手が行った動きr1であるタイプの何かを作成する必要があります。彼らはまた、タイプも彼らが行った動きでr1あるという機能を果たしました。したがって、いずれかのタイプまたはそれらからの何かが必要です。残念ながら、彼らが私たちに与えてくれたのはタイプの何かであり、私たちを勝てない立場に置いています。以前にプレイするのは悪い選択だったと思います。もう一度やり直しましょう...b -> r1bbr1aa
再生r3：r3として再生する場合はr2、関数も再生する必要がありますa -> r3; 幸いなことに、対戦相手はすでにそのような機能を果たしていたので、それを簡単に使用できます。もう一度、他の動きの中に飛び込みます：
b => r1 => a -> (b -> r1) -> r1
...それが以前とまったく同じ不可能な状況であることがわかるだけです。対戦相手の選択に翻弄され、相手がr11つを構築する方法を提供する必要はなく、私たちは閉じ込められたままになります。
おそらく少しのトリックが役立つでしょうか？
ルールを曲げる-遊ぶr1：
通常のHaskellでは、怠惰に頼って物事をひねり、計算に自分の尻尾を飲み込ませることができることを私たちは知っています。方法についてあまり心配することなく、ここで同じことができると想像してみましょうr1。対戦相手が内側のゲームでプレイするものを取り、それを引き出して元に戻し、としてプレイしr2ます。
もう一度、これが対戦相手の動きです：
r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2
私たちの結び目を結ぶシェナニガンの後、それはこれと同等になります：
(b => a -> (b -> r1) -> r1) -> (a -> r1) -> r1
タイプ引数は私たちのトリックのおかげで消えましたが、r1それでも対戦相手によって選択されています。したがって、ここで達成したのは、物事をシャッフルすることだけです。明らかに、これから抜け出すことさえ期待できる方法はないので、私たちは別の行き詰まりにぶつかりました。ar3
したがって、最後の必死の試みを1つ行います。
ルールを曲げる-遊ぶb：
今回bは、最も内側のゲームで対戦相手がプレイしたものをループして、としてプレイしr2ます。これで、対戦相手の動きは次のようになります。
(r1 => a -> (b -> r1) -> r1) -> (a -> b) -> b
そして、内側のゲームに戻ります。
r1 => a -> (b -> r1) -> r1
トリックを続けると、上記の結果をひねってb関数に与え、必要なものb -> r1を受け取るr1ことができます。成功！
一歩下がっても、まだ1つの問題が残っています。タイプの何かをプレイする必要がありa -> bます。明確な方法はありませんが、すでにb嘘をついているので、それを使ってconst、そして-a
- ちょっと待って。bそもそもそのタイプの価値はどこから来ているのでしょうか？相手の立場に立って、相手が手に入れることができるのは、私たちが行った動きの結果だけです。私たちが持っているのが彼らが私たちに与えるものだけである場合、b私たちは輪になって回ることになります。ゲームは決して終わらない。
したがって、のゲームではcallCC、私たちが持っている唯一の戦略は、損失または永続的な膠着状態のいずれかにつながります。
callCC :: forall a. ((a -> (forall b . Cont b)) -> Cont a) -> Cont a
callCC = error "A strange game..."
悲しいかな、唯一の勝利の動きはプレーしないことだと思われます。