Hatena::ブログ(Diary)

まめめも このページをアンテナに追加 RSSフィード

2013-03-03

[] Type-level Quine (未完)

「型システム入門」(TAPL 日本語版)の発売を記念して、型にまつわる何かを書こうと思い、とりあえず型レベルプログラミングでの Quine に挑戦して見ました。

TAPL の内容には全く関係ありません。型クラスは発展的なものなので、入門書である TAPL には名前しか出てきません *1 。型クラスまで書かなくても 500 ページ超の本になるので、型の世界は奥が深いですね。

デモ

ソースはこちら。

ref: https://github.com/mame/type-level-quine/blob/master/type-level-quine-poc.hs

最後の 2 行に注目。

main = putStr $ show quine                                                                  
quine = undefined :: Q X0 b (...) => b

わけわからん型注釈がついてますが、要は quine = undefined なことに注目。

これを以下のようにコンパイルします。

$ ghc -fcontext-stack=2048 type-level-quine-poc.hs
[1 of 1] Compiling Main             ( type-level-quine-poc.hs, type-level-quine-poc.o )
Linking type-level-quine-poc ...

コンパイルには数十秒から数分かかります。また、-fcontext-stack=2048 を付けることに注意。付けないとコンパイラスタックオーバーフローします。

そして生成された実行ファイルを実行すると、

$ ./type-level-quine-poc 
-- Type-level Quine  (c) Yusuke Endoh 2013

-- snip!

main = putStr $ show quine
quine = undefined :: Q X0 b ((X2,Xd):-(X2,Xd):-(X2,X0):-(X5,X4):-(X7,X9):-(X7,X0):-(X6,X5):-(X2,Xd):-(X6,Xc):-(X6,X5):-(X7,X6):-(X6,X5):-(X6,Xc):-(X2,X0):-(X5,X1):-(X7,X5):-(X6,X9):-(X6,Xe):-(X6,X5):-(X2,X0):-(X2,X0):-(X2,X8):-(X6,X3):-(X2,X9):-(X2,X0):-(X5,X9):-(X7,X5):-(X7,X3):-(X7,X5):-(X6,Xb):-(X6,X5):-(X2,X0):-(X4,X5):-(X6,Xe):-(X6,X4):-(X6,Xf):-(X6,X8):-(X2,X0):-(X3,X2):-(X3,X0):-(X3,X1):-(X3,X3):-(X0,Xa):-(X0,Xa):-(X2,Xd):-(X2,Xd):-(X2,X0):-(X7,X3):-(X6,Xe):-(X6,X9):-(X7,X0):-(X2,X1):-(X0,Xa):-(X0,Xa):-(X6,Xd):-(X6,X1):-(X6,X9):-(X6,Xe):-(X2,X0):-(X3,Xd):-(X2,X0):-(X7,X0):-(X7,X5):-(X7,X4):-(X5,X3):-(X7,X4):-(X7,X2):-(X2,X0):-(X2,X4):-(X2,X0):-(X7,X3):-(X6,X8):-(X6,Xf):-(X7,X7):-(X2,X0):-(X7,X1):-(X7,X5):-(X6,X9):-(X6,Xe):-(X6,X5):-(X0,Xa):-(X7,X1):-(X7,X5):-(X6,X9):-(X6,Xe):-(X6,X5):-(X2,X0):-(X3,Xd):-(X2,X0):-(X7,X5):-(X6,Xe):-(X6,X4):-(X6,X5):-(X6,X6):-(X6,X9):-(X6,Xe):-(X6,X5):-(X6,X4):-(X2,X0):-(X3,Xa):-(X3,Xa):-(X2,X0):-(X5,X1):-(X2,X0):-(X5,X8):-(X3,X0):-(X2,X0):-(X6,X2):-(X2,X0):-(X2,X8):-E) => b

(途中を snip! してしまってるのを除けば)めでたく Quine になってます。quine = undefined なのにどうしたことか。

種明かし

インタプリタにかけてみるとわかります。

$ ghci -fcontext-stack=2048 type-level-quine-poc.hs
GHCi, version 7.4.2: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( type-level-quine-poc.hs, interpreted )
Ok, modules loaded: Main.
*Main>

やはり -fcontext-stack=2048 が必要なことに注意。プロンプトが出るまで時間がかかります。

プロンプトが出たら、おもむろに quine の型を見てみます。

*Main> :t quine
quine
  :: (X2, Xd)
     :- ((X2, Xd)
         :- ((X2, X0)
             :- ((X5, X4)
                 :- ((X7, X9)
                     :- ((X7, X0)
                         :- ((X6, X5)
                             :- ((X2, Xd)
                                 :- ((X6, Xc)
                                     :- ((X6, X5)
                                         :- ((X7, X6)
                                             :- ((X6, X5)
                                                 :- ((X6, Xc)
                                                     :- ((X2, X0)
...

中置のコンストラクタを使っているので面食らうかもしれないですが、これは型がリストになっています。Either をリストの cons として使っている感じです (Either head tail のように) 。

このリストの先頭の要素 (すなわち型) は (X2, Xd) です。これは ASCII コードの 0x2d 、つまりハイフンを表しています。その次の要素 (X2, Xd) もハイフン。その次 (X2, X0) は空白。その次 (X5, X4) は T 。同じように解釈を続けて行くと、

-- Type-level ...

というように、ソースコード文字列になっていることがわかります。つまり、quine は項としては undefined だけど型がソースコードを表していたのでした。

コード解説

Quine にするトリックは型クラス Q です。リストの append と Quine の encode を一括しておこなう型レベルの関数として機能しています。

X0 から Xf は nibble (16 進数の 1 文字分) を表しています。型クラス I は、それぞれの nibble を ASCII 文字に変換するための型レベルの関数と、型 X? から対応する整数の値に変換する関数を兼ねています。

文字列を表す型を実際の文字列の値に変換するのは、instance Show のあたりです。

完全な Quine

snip! で省略しない完全な Quine のソースコードは以下。

ref: https://github.com/mame/type-level-quine/blob/master/type-level-quine.hs

quine = undefined の型注釈が長くなったこと以外は poc と同じです。

しかし、このソースをコンパイルしようとするとghc がメモリを食いつぶして OSフリーズするので、動作は確認できていません。コンパイルだけで OS を落とす Quine 。

なので残念ながら未完です。誰かもっと Haskell に詳しい人が効率的に実行できる型レベル Quine を書いてくれることを期待します。

注意 (再掲)

念のためもう一度。この内容は TAPL とは全く関係ありません。

TAPL には、Quine の名前の由来となった Willard Van Orman Quine の著書の引用がちらほらあって何となく嬉しい気持ちになりましたが、もちろん本記事の意味での Quine の話は出てきません。

また、本内容は @keigoi さんの型レベルプログラミング会議の発表内容をちょっと Quine にしてみただけです。なお、@keigoi さんも TAPL の訳者の 1 人です。

本内容とは無関係ですがアフィリエイトを置いておきます。↓クリックするなよ!

型システム入門 −プログラミング言語と型の理論−
Benjamin C. Pierce
オーム社
売り上げランキング: 598

*1:型レベルプログラミングを示唆する記述は 30 章あたりで微妙に出てきます。

amatamat 2013/03/07 16:05 -fcontext-stack=32768
でやってみたらghcが24GBぐらいメモリとスワップ食いつぶして,1時間かけても結局コンパイルできませんでした.ちくしょー.
ご報告まで.

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/ku-ma-me/20130303/p1