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 を書いてくれることを期待します。