型を実行時に作る：怖くないリフレクション #Haskell

この記事は Haskell (その4) Advent Calendar 2017 の19日目の記事です。

この記事は

Oleg Kiselyov and Chung-chien Shan, Functional Pearl: Implicit Configurations -- or, Type Classes Reflect the Values of Types

の劣化版なので、原論文をすでに読んだという人はブラウザーのタブを閉じてくださって結構です。

普通は型と言ったらコンパイル時に決まっているものです¹が、実行時の値に依存した型を作りたい時があります。例えば、 mod n で計算するための型（数学で言う $\mathbf{Z}/n\mathbf{Z}$）を作ったとして、 n として実行時に指定された値を使いたいと言うのは自然な欲求と言えます。

Haskell には、それを実現するための reflection パッケージがあります。（以前、私のブログでも紹介しました）

なになに、「すごそうだけど、どうせ GHC 拡張てんこ盛りなんでしょ」「黒魔術使ってるんでしょ」ですって？

いえいえ、…いや、現在の実装はそうですが、本来は（Haskell の標準機能に加えて）ランク2多相さえあれば「実行時の値に依存した型を作る」ことができます。

では、ランク2多相だけを使って、リフレクションを実装してみましょう。単純さを強調するため、 Prelude 以外のモジュールは使わないことにします。

{-# LANGUAGE Rank2Types #-}

data Proxy a = Proxy

-- ペアノの自然数（型レベル）
data Z
data S n

succProxy :: Proxy n -> Proxy (S n)
succProxy _ = Proxy

predProxy :: Proxy (S n) -> Proxy n
predProxy _ = Proxy

-- 型レベル自然数から値を取り出すための型クラス
class IsNat t where
  reflectNat :: Proxy t -> Integer

instance IsNat Z where
  reflectNat _ = 0

instance (IsNat n) => IsNat (S n) where
  reflectNat p = reflectNat (predProxy p) + 1

-- 実行時の値を使って、型レベル自然数に依存する関数を起動する
reifyNat :: Integer -> (forall n. (IsNat n) => Proxy n -> a) -> a
reifyNat 0 f = f (Proxy :: Proxy Z)
reifyNat n f | n > 0 = reifyNat (n - 1) (\p -> f (succProxy p))

順に解説していきます。

まず、 Proxy は Data.Proxy にあるものと同じです。値を持たない型を取り扱う際、 undefined を扱わなくて済むようにします。

次に、ゼロ Z と後続者 (successor) S によって、型レベルの自然数を定義します。自然数の 1 を表す型は S Z, 2を表す型は S (S Z) という風に、 S の個数で自然数を表します。このほかに、2進表記を使う方法もあります。

succProxy と predProxy はそれぞれ、型レベル自然数に1を加える関数、1減らす関数です。値の文脈で型レベルの操作をしたいので、 Proxy に関する関数としています。ちなみに、 GHC 拡張の ScopedTypeVariables を使えばこれらは不要になります。

その次の IsNat クラスは、型レベル自然数から値を取り出す代物です。ここまでは通常の Haskell です。

次の reifyNat 関数がキモで、ランク2多相を使い、自然数の値を型レベルに持ちあげています。気合いで解読してください。unsafeCoerce のような黒魔術は使っていません。

では実際に使ってみましょう。mod n で計算する型 Modular を実装してみます。

newtype Modular n = M Integer deriving (Eq,Show)

withModuloProxy :: (Proxy n -> Modular n) -> Modular n
withModuloProxy f = f Proxy

instance (IsNat n) => Num (Modular n) where
  negate (M x) = fromInteger (negate x)
  M x + M y = fromInteger (x + y)
  M x * M y = fromInteger (x * y)
  abs x = x
  signum = undefined
  fromInteger x = withModuloProxy (\p -> M (x `mod` reflectNat p))

asModuloProxy :: Modular n -> Proxy n -> Modular n
asModuloProxy = const

-- 型レベル自然数としての 5 と 7
type N5 = S (S (S (S (S Z))))
type N7 = S (S N5)

main = do
  -- まずは、普通に型レベル自然数を使ってみる
  print (reflectNat (Proxy :: Proxy N5))
  print (fromInteger (product [1..6]) :: Modular N7) -- 6の階乗を mod 7 で計算する

  -- 実行時の値としての自然数（10 と 97）を、型レベルに持ち上げて使ってみる
  reifyNat 10 (\p -> print (reflectNat p))
  reifyNat 97 (\p -> print (fromInteger (product [1..96]) `asModuloProxy` p)) -- 96の階乗を mod 97 で計算する

基本はこれだけですが、「型レベル自然数の表記にも 5 とか 42 とかのリテラルを使いたい」や「GHC の実装を悪用して効率よくしたい」などの ~~邪念を抱く~~ 改良を加えると、 GHC 拡張がてんこ盛りになったり黒魔術が出現します。

Swiftにも型クラスっぽいもの（プロトコル）と多相再帰があるので、Swift版も書いてみました→Swiftで型を実行時に作る

静的型付き界隈での「型」の用法です。 ↩