宣伝: 『「シミュレーション仏教」の試み』(JRF 著)。Amazon Kindle で、または、少し高いですが、DRM フリー EPUB を BOOTH で、販売中!
技術系電子本。Python による仏教社会シミュレーション( https://github.com/JRF-2018/simbd )の哲学的解説です。

« Perl でオブジェクト指向 C++風 その3 ローカル関数 | トップページ | aboutme2cocolog: アバウトミーの「ひとこと」をココログプロへ移転するツール »

2011年1月20日 (木)

Haskell の callCC で goto を作る

本稿では、callCC を使ってループを作り、まるで goto のように見えるような動作を構成してみる。Haskell は、強く型付けされた関数型言語だが、十分実用的であって、無限ループも普通に書ける。goto が作れたからと言ってうれしいことはないかもしれないが、その動作がおよそ非直観的で興味深く、これはぜひ紹介したいと考えたのが、本稿を書いた動機である。
callCC は call with current-continuation の略とされ、(callCC (\k ->return (M k))) という形で利用されることが多いだろう。これは、何かを取ってどこかに返す k :: (a->Cont r b) が仮にあるとすると、それを利用した (M k) が k が取るべき引数と同じ型を持つように (M k) :: a を作れば、最初 (M k) を return するが、k という関数に引数が与えられると、その return を「なかったこと」にして、こんどは k に与えられたはずの引数を return したものとして動作する。ややこしいが、例を見ればわかるかもしれない。

この M の構成に抽象データ型を用いて、k を保持するようにもでき、それを利用すれば、k が goto のように作用するループが書ける。以下の example_goto.hs がその例である。

module Main where
import System
import Control.Monad.Cont

data While a b c = LoopEnd a b
                 | LoopStart a b ((While a b c)->c)
                 | Label1 a b ((While a b c)->c)
                 | Label2 a b ((While a b c)->c)

looper input output
  = (callCC $ \goto ->return (LoopStart input output goto));

testloop input = (looper input "") >>= \z -> case z of
  {
    LoopEnd input output -> case input of
       {
         [] -> return (output ++ " lend ");
         c : r -> return (output ++ c ++ " lastnext ");
       };
    LoopStart input output goto -> case input of
      {
        [] -> goto (LoopEnd [] (output ++ " lse "));
        c : r -> goto (Label1 r (output ++ " lsn " ++ c) goto);
      };
    Label1 input output goto -> case input of
      {
        [] -> goto (LoopEnd [] (output ++ " l1e "));
        c : r -> goto (Label2 r (output ++ " l1n " ++ c) goto);
      };
    Label2 input output goto -> case input of
      {
        [] -> goto (LoopEnd [] (output ++ " l2e "));
        c : r -> goto (LoopStart r (output ++ " l2n " ++ c) goto);
      };
  }

main = do runCont (testloop ["a", "b", "c", "d"]) putStrLn


この実行結果は、次のようになる。

Prelude> :load *example_goto
[1 of 1] Compiling Main             ( example_goto.hs, interpreted )
Ok, modules loaded: Main.
*Main> main
 lsn a l1n b l2n c lsn d l1e  lend 


動作を説明しよう。

まず、While という抽象データ型を定義している。これは、上の説明の callCC の k すなわち goto を渡すならば、Either を使った「ラベル付け」だけでは infinite type となるため、それを避けるために必要なものである。

runCont で継続を実行に移し、putStrLn で出力するように指定する。その中の testloop は callCC で作ったものを While に関しケース分けする関数に突っ込んでいる。looper において callCC が「返す」のは、まず LoopStart ラベルが付いたものであると定義している。

input に ["a", "b", "c", "d"] が渡されて、そこから testloop の関数で、文字列に変換していく。LoopStart ラベルが付いたところに来たとき、input のリストの最初のもの c を処理して、output に " lsn " ++ c を継ぎ足し、次のラベル Label1 に goto する。以下、Label1 で "b" が Label2 で "c" が処理され、もう一度 "LoopStart" に戻り "d" が処理されて、Label1 に行く。Label1 ではリストが空になっているので、output に " l1e " を足して、 LoopEnd に goto する。LoopEnd では output に " lend " を足したものを return してループを脱出する。

このとき、callCC が返す「値」が何度も「なかったこと」にされているわけだが、そこの「成果」を一部引き継ぐことには成功すると言える。


ここまでの時点でさえおよそ関数型言語らしくない動作だが、さらにおかしなことが可能となっている。すなわち、goto そのものを return してしまうようなことができるのだ。

通常、ラムダ抽象 (λx. M[x]) の外にその束縛変数 x を出すことはできない。しかし、callCC(\k -> return (M k)) の k はあたかもそれが外に出るかのような定義が許される。以下の example_goto_3.hs がその例である。

module Main where
import System
import Control.Monad.Cont

data While a b m c d = LoopEnd a b
                       ((While a b m c d)->m (c, a -> b -> (d -> m d) -> m c))
                     | LoopStart a b
                       ((While a b m c d)->m (c, a -> b -> (d -> m d) -> m c))
                     | LoopMain a b
                       ((While a b m c d)->m (c, a -> b -> (d -> m d) -> m c))
                     | Method1 a b (d -> m d)
                       ((While a b m c d)->m (c, a -> b -> (d -> m d) -> m c))
                     | Receive1 a b
                       ((While a b m c d)->m (c, a -> b -> (d -> m d) -> m c))
                     | Dummy

looper input output
  = (callCC $ \goto ->return (LoopStart input output goto));

runserver input = (looper input "") >>= \z -> case z of
  {
    LoopEnd input output goto -> case input of
       {
         [] -> return (output ++ " slend ", 
                       (\x y r -> (goto (Method1 x y r goto)) 
                                  >>= \(u, v) -> return u));
         c : r -> return (output ++ c ++ " slastnext ",
                       (\x y r -> (goto (Method1 x y r goto)) 
                                  >>= \(u, v) -> return u));
       };
    LoopStart input output goto -> case input of
      {
        [] -> goto (LoopEnd [] (output ++ " slse ") goto);
        c : r -> goto (LoopStart r (output ++ " slsn " ++ c) goto);
      };

    {- client から要求を受けとる。 -}
    Method1 input output ret goto -> case input of
      {
        [] -> goto (LoopEnd [] (output ++ " sm1e ") goto);
        c : r -> (if (c == "stop") then
                    {- ここから return に向かうこともできる。しかし、
                       そこからどこへ行くのだろう? -}
                   (goto (LoopEnd r (output ++  " sm11e " ++ c) goto))
                 else
                    {- client に結果を送信する。 -}
                    (ret (output ++ " sm1n " ++ c)) >>= (\y -> goto Dummy));
      };
  }

server = runserver [];

runclient input = (looper input "") >>= \z -> case z of
  {
    LoopEnd input output goto -> case input of
       {
         [] -> return (output ++ " clend ", 
                       (\x y r -> (goto (Method1 x y r goto)) 
                                  >>= \(u, v) -> return u));
         c : r -> return (output ++ c ++ " clastnext ",
                       (\x y r -> (goto (Method1 x y r goto)) 
                                  >>= \(u, v) -> return u));
       };
    LoopStart input output goto -> case input of
      {- server の出力を保存する。 -}
      server >>= (\(sout, service)
                  -> goto (LoopMain input (sout ++ output) goto));
    LoopMain input output goto -> case input of
      {
        [] -> goto (LoopEnd [] (output ++ " clme ") goto);
        {- server に [c] を送信して結果を待つ。 -}
        c : r -> server >>= (\(sout, service)
                             -> (service [c] (output ++ " clmn " ++ c)
                                 (\y -> ((goto (Receive1 r y goto))
                                         >>= \(u, v) -> return u))))
                 >>= (\y -> goto Dummy);
      };

    {- server から結果を受けとる。 -}
    Receive1 input output goto -> case input of
      {
        [] -> goto (LoopEnd [] (output ++ " cr1e ") goto);
        c : r -> goto (LoopMain r (output ++ " cr1n " ++ c) goto);
      };
  }

main = do runCont ((runclient ["a", "b", "c", "d", "e"])
                   >>= \(u, v) -> return u) putStrLn


実行結果は以下のようになる。

Prelude> :load *example_goto_3
[1 of 1] Compiling Main             ( example_goto_3.hs, interpreted )
Ok, modules loaded: Main.
*Main> main
 slse  slend  clmn a sm1n a cr1n b clmn c sm1n c cr1n d clmn e sm1n e cr1e  clend 


動作を説明しよう。

まず、最初の例と同様に While という抽象データ型を定義し、infinite type を避けている。goto をそのまま返すことは infinite type になるためできなさそうだが、goto を使うような(一時的な)関数を返すことはできる。

looper の定義は同じ。手抜きで runclient の返す型を runserver のものと同じにしてしまったため、runCont させるとき、返り値(u,v)から goto の部分(v)を削る必要がある。

まず、何も入力せずに runserver で server を起動してあると読める。 server はすでに return され、output として " slse slend " が出る。

client は LoopStart でサーバーの出力を保存し、LoopMain に処理を移す。 LoopMain では、入力されたリストの要素 c を一つ service に渡す。これまでの出力に " clmn " ++ c を足しておく。

このとき、return したはずの server に処理が移る。service には goto Method1 が返されていたので、Method1 の処理になる。ここでは、これまでの出力に " sm1n " ++ c を足す。この c は送られて来たものである。そして、 Method1 の第三引数に指定された client に戻る「復帰」に出力を渡す。

このとき、server は return することなく、client に処理が戻る。client は戻り先の ret に goto Receive1 を指定してあったので、Receive1 の処理になる。Receive1 は渡された値 output の他、元の input も知るよう ret に指定してあった。input のリストから要素 c を取り出した上で、出力に " cr1n " ++ c を足して、LoopMain に goto する。

リストの要素が空になったところで、LoopEnd に行き、出力に " clend " を足して return する。


こんなことができるのである。関数型言語をわざわざ選んで使う方には、とてもいやな感じが伝わると思うがどうだろう?


関連


Haskell のインタプリタは、HaskellPlatform-2010.2.0.0 の WinGHCi を使った。

momo_hs.shar。上のソースの他、callCC に関する例をまとめたアーカイブ。(シェルアーカイブ形式。シェルコマンドとして実行するか unshar を使う。)大きいループから小さいループに移る例もある。

時間泥棒の夕べ》。本稿の姉妹記事。本稿は左の記事の副産物で、その実験中に思い付いたものである。callCC の理論面に関してもそちらで少し書いている。

HaskellのContモナドに触れてみる - Hatena’s Kitchen》。《Call-with-current-continuation - Wikipedia, the free encyclopedia》。Haskell や call/cc を今回はじめて使ってみた。はじめてなのでいろいろなサイトを参考したが、代表して、これらのページを挙げておく。はじめてだったが、他の関数型言語・定理証明器はかなり前に触ったことがあって、その知識が役に立った。

Haskellの継続モナド(Continuation Monad)を理解するポイント - よくわかりません》。投稿後見つけた。Haskell では、特別な実装を行わずにモナドとラムダ抽象をうまく使った遅延評価により「継続」を実現している。その解説がわかりやすかった。
更新: 2011-01-20
初公開: 2011年01月20日 19:37:45
最新版: 2011年01月31日 19:03:12

2011-01-20 19:37:45 (JST) in 関数型言語・定理証明器 | | コメント (2) | トラックバック (1)

批評や挨拶のためのネットコミュニティ

  • はてなブックマーク(って何?) このエントリーをはてなブックマークに追加 このエントリーを含むはてなブックマーク このエントリーを含むはてなブックマーク
  • Twitter (って何?)

トラックバック


トラックバックのポリシー

他サイトなどからこの記事に自薦された関連記事(トラックバック)の一覧です。
» JRF のソフトウェア Tips:Haskell の callCC で goto を作る (この記事)

» 時間泥棒の夕べ from JRF の私見:雑記

「量子」という考え方を御存知あろう。その特徴として、複数の排他的状態が「可能性」として現実に並存し、観測によってその状態が確定する解釈が有名である。喩[たと]えれば、先に書いた七芒星の埋め込みの記事で、平面への展開図が発散する方向は確定していないが、空間への埋め込みにおいては、グラフの作画者はスピンの巻き方を左(InLeft)か右(InRight)に決定せざるをえないようなものだ。 この図のグラフ... 続きを読む

受信: 2011-01-20 19:42:10 (JST)

コメント

更新:リンクを足した。

投稿: JRF | 2011-01-31 19:05:07 (JST)

更新:記事に変更はないが、example_goto_3.hs を少しいじり example_goto_4.hs を作ったので、それを momo_hs.shar に足した。今回のアーカイブは、momo_hs-20110214.shar

goto が返す型に意味がないということを、型変数を残すことで表現しようと考えた。次のような結果になる。(main の出力は example_goto_3.hs と変わらない。)


Prelude> :load *example_goto_4.hs
[1 of 1] Compiling Main ( example_goto_4.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t server
server
:: Cont
(IO ())
(Either [Char] d,
[[Char]]
-> [Char]
-> (Either [Char] d -> Cont (IO ()) d)
-> Cont (IO ()) d)

投稿: JRF | 2011-02-14 16:23:45 (JST)

コメントを書く



(メールアドレス形式)


※匿名投稿を許可しています。ゆるめのコメント管理のポリシーを持っています。この記事にまったく関係のないコメントはこのリンク先で受け付けています。
※暗号化パスワードを設定すれば、後に「削除」、すなわち JavaScript で非表示に設定できます。暗号解読者を気にしないならメールアドレスでもかまいません。この設定は平文のメールで管理者に届きます。
※コメントを書くために漢字[かんじ]でルビが、[google: キーワード] で検索指定が使えます。


ランダムことわざ: 七転び八起き。