型からHello world

Restricted Wordsに参加した。

"Hello World"という文字列を出力するプログラムを、文字・文字列・数値リテラルを使わずに書くという問題。で、回答のコードがこちら。

import Data.Reflection -- cabal install reflection

main = putStrLn $ map toEnum [
      reflect ([] :: [D (D (D (SD (D (D (SD Z))))))])
    , reflect ([] :: [(SD (D (SD (D (D (SD (SD Z)))))))])
    , reflect ([] :: [(D (D (SD (SD (D (SD (SD Z)))))))])
    , reflect ([] :: [(D (D (SD (SD (D (SD (SD Z)))))))])
    , reflect ([] :: [(SD (SD (SD (SD (D (SD (SD Z)))))))])
    , reflect ([] :: [D (D (D (D (D (SD Z)))))])
    , reflect ([] :: [SD (SD (SD (D (SD (D (SD Z))))))])
    , reflect ([] :: [(SD (SD (SD (SD (D (SD (SD Z)))))))])
    , reflect ([] :: [D (SD (D (D (SD (SD (SD Z))))))])
    , reflect ([] :: [(D (D (SD (SD (D (SD (SD Z)))))))])
    , reflect ([] :: [D (D (SD (D (D (SD (SD Z))))))])
    ]

reflectは、型レベルにエンコードされた値を値レベルに戻す関数なのだ。

class Reifies s a | s -> a where
  -- | Recover a value inside a 'reify' context, given a proxy for its
  -- reified type.
  reflect :: proxy s -> a

通常は、なんとunsafeCoerceを駆使してインスタンスを動的に生成するという方法で、値を実行時に型にエンコードするのが普通の使い方。コワイ！だが、Reifiesにはもう一つ、Intのインスタンスもある。

data Z -- 0
data D  (n :: *) -- 2n
data SD (n :: *) -- 2n+1
data PD (n :: *) -- 2n-1

[Z]という型をreflectすると0、[D n]という型をreflectすると2 * n、[SD n]という型をreflectすると2 * n + 1になる。これを利用して、型から自然数を生み出せるのだ。

Prelude Data.Reflection> reflect ([] :: [(D (SD (D (SD (D (SD Z))))))])
42

あとはtoEnum :: Int -> Charで文字に変換して、リストを作ればOK。なんて卑怯純粋で安全な方法！

Given

give :: a -> (Given a => r) -> rという関数は、動的にGivenクラスのインスタンスを生成するgiveで与えた値は、given :: Given a => aによっていつでもどこでも取り出せる。何かと便利だ。