Help us understand the problem. What is going on with this article?

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

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

この記事は

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


普通は型と言ったらコンパイル時に決まっているものです1が、実行時の値に依存した型を作りたい時があります。例えば、 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))

順に解説していきます。

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

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

succProxypredProxy はそれぞれ、型レベル自然数に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で型を実行時に作る


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

Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
Comments
No comments
Sign up for free and join this conversation.
If you already have a Qiita account
Why do not you register as a user and use Qiita more conveniently?
You need to log in to use this function. Qiita can be used more conveniently after logging in.
You seem to be reading articles frequently this month. Qiita can be used more conveniently after logging in.
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
ユーザーは見つかりませんでした