More than 1 year has passed since last update.

GHCの型レベル自然数を理解する

Last updated at 2022-03-24Posted at 2020-04-19

Haskellの多相型システムでは、型をパラメーターとして取る型を定義することができる。この拡張として、GHC拡張の型レベル自然数を使うと、自然数をパラメーターとしてとる型を定義することができる。

型レベル自然数を使うには、GHC拡張の DataKinds を有効にして、 GHC.TypeLits モジュール（もしくは GHC.TypeNats モジュール）をimportする。

この記事で説明するのは基本的に、GHC組み込みの Nat カインドを持つ型レベル自然数である。データ型として帰納的に定義される自然数については、比較のために紹介する程度にとどめる。

初級編

まずは、型レベル自然数の基本的な使い方を紹介する。

雰囲気を掴む

小難しい話に入る前に、GHCの型レベル自然数の雰囲気を見ておこう。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
import Data.Array
import Data.Proxy
import GHC.TypeLits

-- 型レベル自然数によってパラメーター化された行列型
newtype Matrix (n :: Nat) (m :: Nat) a = Mat (Array (Int, Int) a)
  deriving (Eq,Show)

-- 行列乗算（行列のサイズがおかしかったらコンパイルエラーになる）
matMul :: forall a l m n. (Num a, KnownNat l, KnownNat m, KnownNat n)
       => Matrix l m a -> Matrix m n a -> Matrix l n a
matMul (Mat a) (Mat b) =
  Mat $ array ((1,1),(l,n))
              [ ((i,k),v)
              | i <- [1..l]
              , k <- [1..n]
              , let v = sum [ a!(i,j)*b!(j,k) | j <- [1..m] ]
              ]
  where l = fromInteger $ natVal (Proxy :: Proxy l)
        m = fromInteger $ natVal (Proxy :: Proxy m)
        n = fromInteger $ natVal (Proxy :: Proxy n)

-- モジュラー計算の法をパラメーターとして取る型
newtype IntMod (m :: Nat) = IntMod Integer deriving (Eq,Show)

-- モジュラー計算の足し算
-- 法が異なる型同士の演算はさせない
addMod :: KnownNat m => IntMod m -> IntMod m -> IntMod m
addMod t@(IntMod x) (IntMod y) = IntMod ((x + y) `mod` modulus)
  where modulus = natVal t

{-
-- Num のインスタンスも書こうと思えば書ける
instance KnownNat m => Num (IntMod m) where
  ...
-}

main = do
  let a :: Matrix 2 3 Int
      a = Mat $ listArray ((1,1),(2,3))
                          [1,2,3
                          ,4,5,6
                          ]
      b :: Matrix 3 4 Int
      b = Mat $ listArray ((1,1),(3,4))
                          [3,2,1,0
                          ,2,-1,0,3
                          ]
      c :: Matrix 2 4 Int
      c = a `matMul` b -- 行列の積
      -- d = b `matMul` a -- コンパイルエラー

  let x, y :: IntMod 7 -- 型レベル自然数を使って変数を定義する
      z :: IntMod 6
      x = IntMod 3
      y = IntMod 6
      z = IntMod 0
  print $ x `addMod` y -- OK；法が一致している
  -- print $ x `addMod` z -- コンパイルエラー；法の違いが型エラーとなる

使い所

型レベルで自然数が使えるとどういう場面で便利だろうか。

まず、行列のサイズを型で管理できると嬉しい。サイズが一致していない行列同士の足し算やかけ算をコンパイル時に検出できると便利だ。

同様に、ベクターやリストの長さを型レベル自然数で管理できると良いだろう。

また、モジュラー計算の法も典型的な使用例だ。

`Nat` カインド

普通の型と型レベル自然数では、なんというか種類が違う。この「種類」、型の型とでも言うべきもののことをカインド（種）という。

普通の型のカインドは Type であり¹、 Maybe や IO のような「型を受け取る型構築子」のカインドは Type -> Type である。これに対し、型レベル自然数のカインドは Nat である。

例えば、先ほどの Matrix のカインドは Nat -> Nat -> Type -> Type となり、 IntMod のカインドは Nat -> Type となる。

型レベル自然数をパラメーターとして取る型を定義する際は

newtype IntMod (m :: Nat) = ...

という風に型変数に注釈を加える²。型変数のカインド注釈を書くには KindSignatures 拡張が必要である。

なお、 KnownNat 制約が付いている型変数のカインドは Nat と推論されるので、 matMul や addMod 関数の型変数にはカインド注釈を書かなくても良い。あえて書くなら

matMul :: forall a (l :: Nat) (m :: Nat) (n :: Nat)
        . (Num a, KnownNat l, KnownNat m, KnownNat n)
       => Matrix l m a -> Matrix m n a -> Matrix l n a

となる。

リテラル

型レベル自然数を受け取る型に対しては、 x, y :: IntMod 7 や z :: IntMod 6 という風に普通のリテラル表記を使って型レベル自然数を記述できる。DataKinds 拡張のおかげである。

実行時に使える値の取得： `KnownNat` クラス

Haskellでは、型レベルの名前と項レベルの名前は名前空間が完全に分離している。

例えば、型注釈に Int と書けばそれが Int 型と解釈されるが、項レベルの式に Int と買いても「そんなデータ構築子なんて知らん！」と怒られてしまう。型変数についても同じことで、 matMul や addMod の型に m という名前の型変数が出現していても、関数の本体の（項レベルの）式からはそれを自然数の値として参照することはできない。

なので、単に Nat カインドの型変数を使う関数を定義しても、関数の処理の中でそれを使うことはできない。

foo :: forall (n :: Nat). Proxy n -> IO ()
foo _ = print n -- エラー！ n という（項レベルの）変数は存在しない

そもそも、パラメーター多相な関数はどのような型に対しても同じ動作をするものである。仮に

foo :: forall (n :: Nat). IntMod n -> IO ()

という関数があったとして、 foo :: IntMod 42 -> IO () も foo :: IntMod 5000000000000000 -> IO () も同じ動作しかできない。

というわけで、与えられた型レベル自然数を実際に利用するには、単に Nat カインドな型を取るだけのパラメーター多相な関数ではダメだ。Haskellで与えられた型によって異なる挙動をさせるには、そう、型クラスを使う。

与えられた型レベル自然数によって異なる動作をできるようにする、そのための型クラスが KnownNat クラスである。と言っても、 KnownNat クラスは公開されたメソッドを持たない。実際に KnownNat クラスで値を取得するには、 natVal 関数を使う。

GHC.TypeLits

class KnownNat (n :: Nat) where
  ... -- 非公開

natVal :: KnownNat n => proxy n -> Integer

Nat カインドが表すものは普通の型ではないので、 natVal は（直接ではなく）プロキシを介して型レベル自然数を受け取るようになっている。典型的には matMul の例のように Proxy を渡すのだが、 addMod の t :: IntMod m のように型レベル自然数が入った型の値が手元にあるのならそれをそのまま渡せば良い（その場合は proxy = IntMod となる）。

ちなみに、素のHaskellでは matMul :: ... => Matrix l m a -> ... という風な型注釈の中で出てくる型変数を、関数の本体での型注釈（つまり natVal (Proxy :: Proxy l) における :: の右側）で使うことができない。これを可能にするのがGHC拡張の ScopedTypeVariables および forall である。

foo :: KnownNat p => Proxy p -> IO ()
foo _ = print $ natVal (Proxy :: Proxy p) -- エラー！ p は上の行の p とは無関係

-- ScopedTypeVariables の下で
foo' :: forall p. KnownNat p => Proxy p -> IO ()
foo' _ = print $ natVal (Proxy :: Proxy p) -- OK. p は上の行で束縛された型変数を指す

中級編

ここからは、型レベル自然数のより応用的な使い方を見ていこう。

実行時の値を型レベル自然数に持ち上げる

型レベル自然数として使うべき値は、必ずしもコンパイル時に決まらない場合がある。例えば、行列のデータをファイルから読み取る場合や、剰余計算の法を入力のサイズによって適宜変更する場合だ。

C++のテンプレートだったら実行時の値に基づいて型レベル自然数の値を変えるなんてことは「無理！w」で終わりだが、GHCの型レベル自然数では実行時の値を型レベル自然数として利用することができる。

まあ、 Nat カインドの型変数の部分は所詮コンパイル時に消去される飾りにすぎないのでどうでも良い。実行時に実体を持つのは型クラスのインスタンスなので、重要なのは、 KnownNat のインスタンスを実行時に作り出すことである。

実は、 GHC.TypeLits モジュールには KnownNat のインスタンスを実行時に作り出すための型と関数が用意されている。それがこれだ：

GHC.TypeLits

-- SomeNat 型は KnownNat を封じ込めた存在型
data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
{- GADTs風に書けば
data SomeNat where
  SomeNat :: KnownNat n => Proxy n -> SomeNat
-}

someNatVal :: Integer -> Maybe SomeNat
someNatVal n
  | n < 0 = Nothing
  | n >= 0 = Just (SomeNat (Proxy :: Proxy ???)) -- compiler magic で n に対応する KnownNat を生成する

SomeNat 型は存在型と呼ばれるやつである。SomeNat 型の値を SomeNat データ構築子にパターンマッチさせることによって、何らかの型 n に関する KnownNat n 制約をスコープに持ち込むことができる。要は SomeNat 型は型レベル自然数を封じ込めたデータ型だと思えば良い。

何らかの方法で SomeNat 型を入手できた場合の使い方も見ておこう。一番簡単な、「型レベル自然数の値を表示する」コードは次のようになる：

case ??? :: SomeNat of
  SomeNat proxy ->
    -- proxy は何らかの n に対する Proxy n 型である。
    -- n に関しては KnownNat n という制約が利用できる。
    natVal proxy

あるいは、 ScopedTypeVariables 拡張の下では次のように書くこともできる。

case ??? :: SomeNat of
  SomeNat (_ :: Proxy n) ->
    -- パターンマッチにより n という型変数を新たに導入する。
    -- n に関しては KnownNat n という制約が利用できる。
    natVal (Proxy :: Proxy n)

SomeNat 型の使い方はわかったので、次は SomeNat 型の値の作り方だ。勘のいい読者はすでに気づいていると思うが、GHC.TypeLits の someNatVal 関数を使うと実行時の値を元にして型レベル自然数を作ることができる。someNatVal 関数の入力は Integer で、入力が負の場合に対応するために返り値は Maybe に包まれている。

まとめると、実行時に与えられた自然数を元にして型レベル自然数を使うコードは、例えば次のようになる：

{-# LANGUAGE DataKinds #-}
import GHC.TypeLits
import Data.Proxy

-- 型レベル自然数を利用する関数
foo :: KnownNat n => Proxy n -> IO ()
foo proxy = putStrLn $ "入力は " ++ show (natVal proxy) ++ " ですね！"

main = do
  n <- readLn
  -- 標準入力から読み取った Integer から型レベル自然数を作る
  case someNatVal n of
    Nothing -> error "ﾃﾒｯｺﾗｰ！自然数を入力しやがれｺﾗｰ！"
    Just (SomeNat proxy) -> foo proxy

「実行時の値を元にした型レベル自然数を作る」ことに関しては、reflectionパッケージの Data.Reflection モジュールにもそのための関数がある。こちらは存在型の代わりにrank-2 typeを使っている。

Data.Reflection

reifyNat :: forall r. Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r

someNatVal と reifyNat のどちらを使うのが良いかという点に関して、筆者の意見を述べておこう。Nat カインドや KnownNat はGHCに密接した機能であり、GHCのバージョンが変わると実装が変わる可能性がある³。それを考えると、reflectionパッケージよりは、GHC本体に付属する SomeNat/someNatVal を使った方が新しい実装でも問題なく動く可能性が高い。

一方で、「そもそも GHC.TypeLits は安定したAPIと呼べるのか⁴」という問題もあり、サードパーティーのライブラリーの方がGHCのバージョン違いを吸収しやすいのではないか、という考え方もあるかもしれない。

まあ、GHCの型レベル自然数の機能自体がまだ未成熟（後述の問題点もあるし）と割り切って、型レベル自然数を使う際はGHCの新バージョンが出るたびに動作チェックを行う、という態度が一番安全だろう。

Integer vs Natural

これまでに紹介した natVal 関数や someNatVal 関数が「型レベル自然数の実行時の値」として受け渡しするものは整数型 Integer だった。

しかし、最近の GHC（GHC 7.10 / base-4.8.0.0 以降）には自然数を表す Natural 型がある。型レベル「自然数」というからには natVal 関数や someNatVal 関数は Natural 型を扱うようにするべきではないのか？

というわけで、GHC 8.2 (base-4.10.0.0) からは GHC.TypeNats モジュールが用意されていて、そこで用意されている natVal 関数や someNatVal 関数は Natural 型を扱うようになっている。GHC.TypeLits の関数の型は Integer のままなので、既存のコードはそのまま GHC 8.2 以降でも動く。

GHC.TypeNats

-- Integer / Natural が絡まない型や関数については GHC.TypeLits と GHC.TypeNats で同一のものが（再）エクスポートされている
data Nat
class KnownNat (n :: Nat)
data SomeNat where ...

-- GHC.TypeNats の natVal と someNatVal は Integer の代わりに Natural を使う
natVal :: KnownNat n => proxy n -> Natural
someNatVal :: Natural -> SomeNat

特に、 GHC.TypeLits の someNatVal は入力が負の可能性を考慮して Maybe に包んだ値を返すようになっていたが、 GHC.TypeNats の方は入力が自然数であるとわかっているので直接 SomeNat を返すようになっている。

Nat や KnownNat, SomeNat などの、Integer vs Natural の違いの影響を受けない型は GHC.TypeLits と GHC.TypeNats で同じものが（再）エクスポートされている。「Integer 用の KnownNat と Natural 用の KnownNat があって紛らわしい」なんてことはないので安心してほしい。

等価性の比較： `sameNat`

「関数の型に含まれる型レベル自然数のアレとコレが等しい」ことを要求するには、そういう風な型を書けばよかった。最初の例でいう matMul は1つ目の行列の列の数と2つ目の行列の行の数が等しいことを要求するが、そこに同じ変数 m を使うことによって要求を表現している。

一方で、「必ずしも等しいとは限らない型レベル自然数2個を（実行時に）比較したい」場合はどう書けば良いだろうか。

例として、 matMul の入力が緩い版、つまり「行列のサイズが噛み合っていれば行列乗算をして、噛み合っていなければ Nothing を返す」関数を定義してみよう。

matMul' :: forall l m m' n a
         . (Num a, KnownNat l, KnownNat m, KnownNat m', KnownNat n)
        => Matrix l m a -> Matrix m' n a -> Maybe (Matrix l n a)

まず考えられる実装方法は、 natVal で値を取得して普通に == で比較することだろう。

matMul' a b = if m == m' then -- 行列のサイズが噛み合っていれば
                Just (matMul a b) -- 呼び出せてもいいはず、だけど……コンパイルエラー！
              else
                Nothing
  where m = natVal (Proxy :: Proxy m)
        m' = natVal (Proxy :: Proxy m')

だが、これはうまくいかない。「Couldn't match type ‘m'’ with ‘m’」という型エラーが出るはずだ。

型のない言語ではもちろんこんなエラーは出ない。あるいは、TypeScript等の言語は（行列乗算の例に適用できるかは別として） == や instanceof 等の一部の演算子を特別扱いして条件に応じて型を変えるということをやってくれる。しかし、Haskellでは比較演算と型検査器はそこまで密結合していないのだ。

しかし安心してほしい。HaskellにはHaskellのやり方があるのだ。上記の matMul' を改修すれば、「行列のサイズがあっていれば matMul を呼び出す」という望み通りの挙動を実現できる。

2つの型レベル自然数の等価性を判定して、等しい場合にそれらを同じ型として扱うには、 sameNat 関数を使う。sameNat 関数は、2つの型レベル自然数が等しければその証拠を Just に包んで返す。

GHC.TypeLits

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)

「証拠」というのは、a :~: b というデータ型の値だ。:~: 型は型レベルの等式である「~ 制約」を封じ込めたGADTsとでも言うべきだろうか。a と b が等しい型である場合に限り、 a :~: b は停止する値 Refl を持つ。a :~: b 型の値にパターンマッチをして Refl が取り出せれば、その部分では a と b は同じ型として扱われる。

Data.Type.Equality

data a :~: b where
  Refl :: a :~: a

これを使うと先ほどの matMul' は次のように実装できる。

-- GADTs 拡張を有効にして、 "import Data.Type.Equality" を加える
matMul' a b = case sameNat (Proxy :: Proxy m) (Proxy :: Proxy m') of
                Nothing -> Nothing -- m と m' は異なる
                Just Refl ->
                  -- m と m' は等しい。以後、 m と m' は同じ型として扱われる。
                  Just $ matMul a b

型レベル計算

GHC.TypeLits （あるいは GHC.TypeNats）は、足し算や掛け算などの型レベル自然数に関する操作（型レベル関数）を提供している。

型レベル演算子を有効にするには、 TypeOperators 拡張および NoStarIsType 拡張を有効にする。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators, NoStarIsType #-}
import GHC.TypeLits
import Data.Proxy

proxy1 :: Proxy (2 * 3)
proxy1 = Proxy

proxy2 :: Proxy (3 + 3)
proxy2 = Proxy

proxy3 :: Proxy 5
proxy3 = Proxy

main = do
  print (proxy1 == proxy2) -- proxy1 と proxy2 の型は等しいので、コンパイルが通る
  -- print (proxy1 == proxy3) -- proxy1 と proxy3 の型は異なるので、コンパイルが通らない

GHC.TypeLits および GHC.TypeNats で提供されている型レベル関数（演算子）は、次の通りである。

GHC.TypeNats

type (<=) :: Nat -> Nat -> Constraint
type (<=?) :: Nat -> Nat -> Bool
type (+) :: Nat -> Nat -> Nat
type (*) :: Nat -> Nat -> Nat
type (^) :: Nat -> Nat -> Nat
type (-) :: Nat -> Nat -> Nat
type CmpNat :: Nat -> Nat -> Ordering
type Div :: Nat -> Nat -> Nat
type Mod :: Nat -> Nat -> Nat
type Log2 :: Nat -> Nat

これらを使うと、例えば「特定の範囲の型レベル自然数を取る関数」というのも書ける。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
import GHC.TypeLits
import Data.Proxy

-- 2以上7以下の型レベル自然数を受け取る関数
hoge :: (KnownNat a, 2 <= a, a <= 7) => Proxy a -> IO ()
hoge proxy = print $ natVal proxy

main = do
  -- hoge (Proxy :: Proxy 1) -- コンパイルが通らない
  -- hoge (Proxy :: Proxy 10) -- コンパイルが通らない
  hoge (Proxy :: Proxy 2) -- コンパイルが通る

型レベル計算の限界：自然数の等式

型変数を含む式に関しても型演算を使うことができる（ように見える）。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators, NoStarIsType #-}
import GHC.TypeLits
import Data.Proxy

double1 :: forall (n :: Nat). Proxy n -> Proxy (2 * n)
double1 Proxy = Proxy

double2 :: forall (n :: Nat). Proxy n -> Proxy (n + n)
double2 Proxy = Proxy

main = do
  print (double1 (Proxy :: Proxy 3) == double2 (Proxy :: Proxy 3)) -- コンパイルが通る

しかし、次のコードはどうだろうか。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators, NoStarIsType #-}
import GHC.TypeLits
import Data.Proxy

double1 :: forall (n :: Nat). Proxy n -> Proxy (2 * n)
double1 Proxy = Proxy

double2 :: forall (n :: Nat). Proxy n -> Proxy (n + n)
double2 Proxy = Proxy

test :: forall (n :: Nat). KnownNat n => Proxy n -> Bool
test proxy = double1 proxy == double2 proxy -- Proxy (2 * n) と Proxy (n + n) を比較している

main = do
  print $ test (Proxy :: Proxy 3) -- 一見すると先ほどと同じ意味のコードだが……？

残念ながらこのコードの test 関数はコンパイルが通らない。「2 * n と n + n の型が一致しない」という風なエラーが出るはずだ。

    • Couldn't match type ‘2 * n’ with ‘n + n’
      Expected type: Proxy (2 * n)
        Actual type: Proxy (n + n)

実は、型レベル関数（演算子）の能力は型変数が含まれると大きく低下する。

GHCは、型チェックの段階で具体的な型レベル自然数の値がわかっていればそれを計算（簡約）することにより 2 * 3 と 3 + 3 が等しいことを納得できる。しかし、型変数の値が具体的にわからない場合はそういう計算はできないし、自然数の性質（例えば 2 * n == n + n であること）も知らないので、 2 * n と n + n が同じ型であることはわからないのだ。

先の例

main = do
  print (double1 (Proxy :: Proxy 3) == double2 (Proxy :: Proxy 3)) -- コンパイルが通る

のコンパイルが通ったのは、比較を行っている main 関数の中では double1 (...) の型は Proxy (2 * 3) で、 double2 (...) の型は Proxy (3 + 3) であることがわかっていたからだ。具体的な値がわかっていればGHCは実際の値を計算できるので型検査が通る。

ちなみに、自然数の足し算の可換性などもGHCは「知らない」。すなわち、 a + b と b + a は等しい型とはみなされない。

ちなみに、GHCが自然数の法則を全く知らないかと言うとそうでもなくて、 a + 0 と a を同一視したり、 (a + 2) ~ 5 という制約から a ~ 3 を導出するようなことは行ってくれるらしい（GHC 7.8 以降）。

1.5. Release notes for version 7.8.1

型レベル計算の限界その2：`KnownNat` のインスタンス

GHCの型レベル自然数に関する別の問題として、「型レベル自然数の演算結果が KnownNat のインスタンスにならない」という問題がある。

例えば、次のコードを考えてみよう。

foo :: forall n. KnownNat n => Proxy n -> IO ()
foo _ = do
  let p :: Proxy (n + 1)
      p = Proxy
  print (natVal p) -- n + 1 が計算されてほしいが……エラー！

natVal p を呼び出すには n + 1 が KnownNat のインスタンスである必要がある。n に関しては KnownNat n 制約があるので、GHCの側で n + 1 に対応する KnownNat を導出してくれても良さそうなものだが……残念ながら、現行のGHCではそういうことはしてくれない。

GHCの `Nat` は帰納的な定義ではない

GHCの型レベル自然数の計算が型変数を含むとうまくいかなくなるのは、GHCの型レベル自然数の中身がブラックボックスな割にGHC自身の自然数に関する知識が乏しいからだ。

GHC組み込みの Nat ではなく、独自に型レベル自然数を定義すれば、この手の問題は発生しない。例えば、ペアノ流に自然数を

data Nat = Z | S Nat

type family (x :: Nat) + (y :: Nat) where
  Z + y = y
  S x + y = S (x + y)

と定義するというやり方が考えられる。実際、finパッケージではそのように定義された Nat 型（カインド）を提供している。

帰納的に定義した型レベル自然数であれば、

自然数の性質を自力で証明する。つまり、 Proxy x -> Proxy y -> x + y :~: y + x のような関数を定義する。
演算の結果に対する KnownNat の相当物を自力で導出する。

ことが unsafeCoerce を使わずに可能となる。

デメリットは、

ペアノ自然数の場合、自然数の大きさに応じたコストがかかる。
- 演算について、入力のサイズに応じた計算時間がかかる。例えば足し算は O(nm) となる。
- そもそも大きな数を型レベルペアノ自然数で表そうとした時点でGHCが音を上げるので、演算のコストは問題とはならないかもしれない。

である。ペアノ自然数の代わりに位取り記数法みたいなやつを使えば計算量のオーダーは削減できるかもしれない。

この記事の主題は「GHC組み込みの Nat」なので、独自に定義する型レベル自然数およびそれを使った定理証明についてはこれ以上は取り扱わない。

型レベル計算の限界を克服する

先述の通り、GHC組み込みの型レベル自然数（Nat カインド）は未熟、未完成である。そのため、それを補うライブラリーやコンパイラープラグインが開発されている。

要約：コンパイラープラグインを使え。

ライブラリーの利用

「演算結果に対する KnownNat がない」という問題に対しては、singletonsパッケージが利用できる。

まず、Haskellコードで

instance (KnownNat a, KnownNat b) => KnownNat (a + b)

という風なインスタンスを定義することはできない。KnownNat のメソッドは公開されていない上に、 + は型構築子ではないからだ。（実際にやってみると Class ‘KnownNat’ does not support user-specified instance という専用のエラーメッセージが出る。）

ではライブラリーとして何ができるかというと、「KnownNat を封じ込めたデータ型」を用意してそれを返す関数を定義する、という事になる。

「KnownNat を封じ込めたデータ型」としては SomeNat がすでに登場したが、あちらは「素性の知れない型レベル自然数に対する KnownNat」を封じ込めているのに対し、今回必要なのは「a + b という具体的な型レベル自然数に対する KnownNat」を封じ込める型だ。

つまり、次のようなデータ型を用意する（このデータ型は実際に singletons パッケージが提供している）。

Data.Singletons.TypeLits

-- n に関する KnownNat を「封じ込めた」データ型、あるいは n が KnownNat である「証拠」となるデータ型
data SNat (n :: Nat) = KnownNat n => SNat
{- GADTs風に書けば
data SNat (n :: Nat) where
  SNat :: KnownNat n => SNat n
-}

SNat n 型の値は、型レベル自然数 n に対応する KnownNat のインスタンスを封じ込めている。

これを使って、singletonsパッケージは例えば次のような関数を用意している。

Data.Singletons.Prelude.Num

(%+) :: SNat x -> SNat y -> SNat (x + y)
(%-) :: SNat x -> SNat y -> SNat (x - y)
(%*) :: SNat x -> SNat y -> SNat (x * y)

つまり、 (%+) を使えば KnownNat (x + y) が得られるわけだ。使用例は次のようになる：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators, NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Proxy
import Data.Singletons.Prelude.Num ((%+), type (+))
import Data.Singletons.TypeLits (SNat(..))
import GHC.TypeNats (KnownNat, natVal)
-- GHC.TypeNats のエクスポートする type (+) と singletons のエクスポートする type (+) は衝突するので注意

foo :: forall n. KnownNat n => Proxy n -> IO ()
foo _ = do
  let p :: Proxy (n + 1)
      p = Proxy
  case (SNat :: SNat n) %+ (SNat :: SNat 1) of
    SNat {- SNat (n + 1) -} ->
      -- KnownNat (n + 1) が使える！
      print (natVal p)
{-
  TypeApplications の下では Data.Singletons.sing を使って
  case sing @n %+ sing @1 of
    SNat {- SNat (n + 1) -} ->
      print (natVal p)
  と書くこともできる
-}

singletonsパッケージはTemplate Haskellによるコード生成やカインド多相の利用を大々的に行っており、Haddockを見ても様子がわかりにくい。関数の型を見るときはGHCiで :t (%+) @Nat と言う風にした方がいいかもしれない。ここでは、関数を Nat カインドに特化させた場合の型をいくつか紹介しておく。

Data.Singletons.Prelude.Num

(%+) :: SNat x -> SNat y -> SNat (x + y)
(%-) :: SNat x -> SNat y -> SNat (x - y)
(%*) :: SNat x -> SNat y -> SNat (x * y)

-- 以下の型関数は GHC.TypeLits のものとは定義が異なる（より一般化されている）ので注意。
-- Nat について適用した結果は GHC.TypeLits のものと同じ型を返す。
type (+) :: Nat -> Nat -> Nat
type (-) :: Nat -> Nat -> Nat
type (*) :: Nat -> Nat -> Nat

Data.Singletons.TypeLits

data SNat n = KnownNat n => SNat
withKnownNat :: SNat n -> (KnownNat n => r) -> r
(%^) :: SNat x -> SNat y -> SNat (x ^ y)
(%<=?) :: SNat a -> SNat b -> SBool (a <=? b)
sLog2 :: SNat x -> SNat (Log2 x)
sDiv :: SNat x -> SNat y -> SNat (Div x y)
sMod :: SNat x -> SNat y -> SNat (Mod x y)
type DivMod :: Nat -> Nat -> (Nat, Nat)
sDivMod :: SNat x -> SNat y -> STuple2 '(Div x y, Mod x y)
-- quot/rem の対応物もあるが、自然数についてはこれらは div/mod と同じなので省略
-- このほか、 GHC.TypeLits からの再エクスポートがいくつかある

Data.Singletons.Prelude

data SOrdering (a :: Ordering) where
  SLT :: SOrdering 'LT
  SEQ :: SOrdering 'EQ
  SGT :: SOrdering 'GT

data SBool (a :: Bool) where
  SFalse :: SBool 'False
  STrue :: SBool 'True

Data.Singletons.Prelude.Ord

sCompare :: SNat x -> SNat y -> SOrdering (CmpNat x y)

型演算の結果に対する KnownNat が欲しいけどsingletonsは大掛かりすぎる、という場合には、もう少し小さいライブラリとして typelits-witnesses があるようだ。

compiler pluginによる解決

GHCが自然数についての等式 2 * n = n + n や a + b = b + a を「知らない」のであれば、コンパイラーを拡張して知識を補ってやれば良い。そういうわけで、GHCの型レベル自然数についての能力を強化するためのコンパイラープラグインがいくつか存在する。

ghc-typelits-natnormalise
- 型レベル自然数の等式を解決する。
ghc-typelits-presburger
- 型レベル自然数の等式を解決する。
- 使用の際には equational-reasoning も依存関係に加える必要があるようだ。Issue: Requires equational-reasoning at runtime #2
ghc-typelits-knownnat
- 「演算結果に対する KnownNat が推論されない」という問題を解決する。
type-nat-solver
- SMTソルバーを利用するらしい。
- Hackageに上がっていない。
- GHC 8.8.3 では動作しなかった。

例えば、 ghc-typelits-natnormalise を使う場合はパッケージの依存関係に ghc-typelits-natnormalise を加えて、型レベル自然数を使いたいモジュールの冒頭に

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

を書き加える。簡単だ。他のプラグインも同様である。

コンパイラープラグインはGHCに密に依存するので、GHCのバージョンが変わると動作しなくなる可能性がある。採用する際は継続的に開発されていることを確認するか、自力で最新のGHCに対応させる覚悟を持つようにしよう。この辺はOSSを使うときの一般論だが、GHCプラグインの場合は特に、だ。

ちなみに筆者がGHC 8.8.3で試したところ、ここで紹介したプラグインの中でtype-nat-solver以外の3つは動作した（簡単な動作確認しか行っていないが）。

この他、 GHC.TypeLits で提供されていない型演算とそれ用のGHCプラグインをセットで提供するパッケージもあるようだ (ghc-typelits-extra)。

黒魔術編

最後に、ライブラリーやコンパイラープラグインに頼らずに自前でどうにかする方法を紹介する。ここまでくると黒魔術全開なので、心臓の弱い方、Haskellに未だ憧れを持っている方はこのセクションは読み飛ばすことをお勧めする。

まず、GHCの能力不足を自前で補うための基本方針は、「unsafeCoerce を使って型システムをかいくぐる」となる。

「unsafeCoerce を使うやり方がまともとは思えない！」と思ったあなたはまともな感性の持ち主だ。その気持ちを大事にしてほしい。

とは言っても、GHC組み込みの型レベル自然数はブラックボックスなので、型レベル自然数の非自明な等式を利用したり、演算結果に対する KnownNat のインスタンスを得るには本当にこれくらいしかやりようがないのだ。

ちなみに、先に紹介したsingletonsの Nat に対する関数も、結局のところ内部的には unsafeCoerce を使って実装されていたりする。

GHCに型レベル自然数の等価性を納得してもらう

まずは、「等価と判断されてほしい型が等価にならない」問題をどうにかする。

例えば、 a + b と b + a が等価であることをGHCに納得させたい、としよう。そのためには

commutativity :: Proxy a -> Proxy b -> a + b :~: b + a
commutativity _ _ = {- なんらかの方法で Refl を返す -}

という（停止する）関数を作れば、目的は達成できる。（引数の Proxy は、型を曖昧にしないために必要となる。 AllowAmbiguousTypes 拡張を使えば Proxy 引数を省けるが、個人的には AllowAmbiguousTypes は好きではないので、この記事では使わない。）

先に述べた通り、GHCの Nat カインドは帰納的な定義ではないので、型レベル自然数についての性質を真っ当に証明する、ということができない。

なので、ここは「ずる」をする。すなわち、 unsafeCoerce を使って型システムを誤魔化す。

commutativity :: Proxy a -> Proxy b -> a + b :~: b + a
commutativity _ _ = unsafeCoerce Refl
{-
GHCが自然数の性質を知っていれば
commutativity _ _ = Refl
で済むのだが……
-}

ちなみに、 sameNat のソースを見ると、そこでも unsafeCoerce Refl を使って a :~: b の値を作っていた。

型レベル自然数の演算結果の `KnownNat` を自前で用意する

「a と b に対する KnownNat があっても a + b は KnownNat にならない」という問題を自前で解決することを考える。方針は

項レベルの計算によって目的の値を作り出す
someNatVal によって目的の値を持った KnownNat のインスタンスを作る。ただし SomeNat の中の型変数（SomeNat (_ :: Proxy m) の m）は未知の型である。
型検査器を騙して、未知の型と目的の型レベル自然数 a + b が同じ型だと思い込ませる。

となる。

-- 要 ScopedTypeVariables

-- n が KnownNat である「証拠」を保持するデータ型
data SNat (n :: Nat) where
  SNat :: KnownNat n => SNat n

-- 与えられた型レベル自然数の和が KnownNat である「証拠」を返す関数
add :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> SNat (a + b)
add proxyA proxyB =
  let a = natVal proxyA
      b = natVal proxyB
      c = a + b -- とりあえず項レベルの計算をする
  in case someNatVal c of -- 目的の値を持つ KnownNat のインスタンスを用意する
       SomeNat (_ :: Proxy c) ->
         -- ここでは型 c は KnownNat のインスタンスとなっているが、
         -- この時点では型 c と型 a + b は無関係
         unsafeCoerce (SNat :: SNat c) -- SNat c と SNat (a + b) が同じ型だと思い込ませる

応用：型レベル素数判定

型レベルプログラミングに慣れた方なら、型レベルで素数判定を行いたくなるのは自然だろう。ある種のアルゴリズムには素数が必要だし、「与えられた型レベル自然数が素数である」という要求を型制約として書けるのはとても素敵なことだ。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators, NoStarIsType #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
import GHC.TypeLits
import Data.Proxy

-- 素数判定の型レベル関数
type family IsPrime (n :: Nat) where
  IsPrime 0 = False
  IsPrime 1 = False
  IsPrime 2 = True
  IsPrime n = IsPrimeLoop n 3 (Mod n 2) (CmpNat n 2)

type family IsPrimeLoop (n :: Nat) (d :: Nat) (r :: Nat) (b :: Ordering) where
  IsPrimeLoop n d _ LT = True
  IsPrimeLoop n d 0 _ = False
  IsPrimeLoop n d _ _ = IsPrimeLoop n (d + 2) (Mod n d) (CmpNat n (d * d))

-- 法が素数である、ということを型レベルで要求する関数
invMod :: forall p. (KnownNat p, IsPrime p ~ True) => IntMod p -> IntMod p
invMod x = x^(p-2) -- Fermatの小定理
  where p = natVal x

newtype IntMod (m :: Nat) = ...
instance KnownNat m => Num (IntMod m) where ...

main = do
  print $ invMod (3 :: IntMod 7) -- コンパイルが通る
  -- print $ invMod (3 :: IntMod 6) -- コンパイルが通らない

しかし、使う自然数がコンパイル時に決まっている場合はともかく、「実行時に入力された、あるいは乱数で生成した素数を型レベルに持ち上げて処理を行う」という場合にはHaskellの型レベルプログラミングは無力だ。まともな依存型のある言語ならどうだか知らないが、Haskellでは真っ当な方法では不可能だ。

-- 素数判定（手抜き）
isPrime :: Integer -> Bool
isPrime n | n <= 1 = False
          | otherwise = all (\m -> n `rem` m /= 0) [2..n-1]

main = do
  print $ invMod (3 :: IntMod 7) -- コンパイル時にわかっている型レベル自然数なら良いが……
  n <- readLn
  if isPrime n then
    case someNatVal n of
      Nothing -> undefined
      Just (SomeNat (_ :: Proxy p)) ->
        -- 実行時に作った型レベル自然数に対する IsPrime p がどうなるかはコンパイラにはわからない！
        print $ invMod (3 :: IntMod p) -- エラー！
  else
    putStrLn "入力されたのは素数ではなかったよ😢"

これをどうにかするには、「与えられた自然数が素数であるか実行時チェックを行い、素数であればその証拠を返す」ような関数を定義し、それを素数判定に使う。

「素数である証拠」というのは、型制約としての IsPrime p ~ True をデータ型に封じ込めたものであり、具体的には IsPrime p :~: True 型の値である。この値は例によって真っ当な方法では作れないので、 unsafeCoerce を利用する。

-- 素数判定（手抜き）
isPrime :: Integer -> Bool
isPrime n | n <= 1 = False
          | otherwise = all (\m -> n `rem` m /= 0) [2..n-1]

-- 素数判定（型レベルの保証付）
isPrime' :: KnownNat n => Proxy n -> Maybe (IsPrime n :~: True)
isPrime' proxy | isPrime (natVal proxy) = Just (unsafeCoerce Refl)
               | otherwise = Nothing

main = do
  n <- readLn
  case someNatVal n of
    Nothing -> putStrLn "入力されたのは自然数ではなかったよ😢"
    Just (SomeNat (proxy :: Proxy p)) ->
      -- この時点で KnownNat p が手に入る
      case isPrime' proxy of
        Nothing -> putStrLn "入力されたのは素数ではなかったよ😢"
        Just Refl ->
          -- この時点で IsPrime p ~ True となる
          print $ invMod (3 :: IntMod p)

この例では「型レベル関数 IsPrime」と「通常の関数 isPrime」と「通常の関数に型システム用の証拠を組み合わせた関数 isPrime'」の3つの定義する必要があり、正直煩雑である。singletonsパッケージを利用すればこういうボイラープレートを削減できるのかもしれないし、陽に unsafeCoerce を書かなくて良くなるのかもしれない（筆者はあまりsingletonsパッケージを使ったことはないので、これ以上はなんとも言えない）。

（まあ、singletonsパッケージを使わずに手書きすることには、「型レベルの関数 IsPrime と項レベルの関数 isPrime で必ずしも同じアルゴリズムを使う必要がない」というメリットもあるかもしれない。）

GHC組み込みの型レベル自然数（Nat カインド）関連で面白いことをやっている日本語記事をいくつか探してみたのでリンクを貼っておく。

@myuon_myon, GHC.TypeLitsと型レベルFizzBuzz (2014年10月)
@mod_poppo, Haskell (GHC) の型レベル自然数とリフレクションを試してみる (2016年10月)
@autotaker1984, コンパイル時に素数判定を行ってみた (2019年3月)
@masahiro_sakai, テンソル形状のコンパイル時検査＋実行時アサーション化を今のHaskellで書いてみる (2019年10月)
@YoshikuniJujo, GHCのタイプチェックプラグインについて、すこし (2019年10月)

それから、GHCに Nat が導入された頃の議論へのリンクも貼っておく：

おまけ：`Symbol` カインド

GHCには型レベル文字列とでも言うべき Symbol カインドというものもある。Symbol カインドも GHC.TypeLits で定義されており、対応する（項レベルの？）型は String となる。

この記事を読んでGHCの型レベル自然数の使い方がわかった方ならば、シンボルの方も類推で使えるだろう。Nat と Symbol の対応表を載せておく。

	型レベル自然数	型レベル文字列（シンボル）
カインド	`Nat`	`Symbol`
型クラス	`KnownNat`	`KnownSymbol`
実行時の対応物	`Integer` または `Natural`	`String`
値の取得	`natVal`	`symbolVal`
	`SomeNat`	`SomeSymbol`
実行時の値の持ち上げ	`someNatVal`	`someSymbolVal`
等価性の判定	`sameNat`	`sameSymbol`

Nat に対しては + や * などの型関数があったが、 Symbol に対しても AppendSymbol という型関数が用意されている。

追記：`Nat` 型と `Natural` 型

これまで「Nat カインド」という言い方をしてきたが、ドキュメントを見ると data Nat と書かれている。実は、GHC的には Nat はあくまで「型」で、それをDataKinds拡張で持ち上げたものが Nat カインド、という扱いなのだ。とはいえ、 Nat 型は停止する値を持たないので、普通の型としては使いどころがない。

さて、自然数を表す型としては、 Nat の他に Numeric.Natural モジュールで定義されている Natural 型がある。Nat 型はカインドとして使うのが主な用途で、 Natural 型は通常の型として使うのが主な用途だ。この二つの用途はかぶらないので、 Nat 型と Natural 型は統合しても良さそうである。

実際にGHC 9.2では Nat と Natural は統合され、 type Nat = Natural となった。

以前は「普通の型」のカインドは * と表記されていたが、型とカインドが統合される流れの中で * は型演算子と紛らわしいので、普通の型のカインドとしては Data.Kind モジュールの Type を使う方が良さそうだ。 ↩
GHC 8.10 以降では StandaloneKindSignatures 拡張で type IntMod :: Nat -> Type; newtype IntMod m = ... と書くこともできる。 ↩
GHC 8.2では実際に KnownNat の内部表現が変わり、reflectionパッケージの reifyNat が誤動作をしていた（当該issue）。reflectionパッケージの最新リリース (2.1.5) では修正済み。 ↩
GHC.TypeLits 登場当初の GHC 7.6 (base-4.6) と次のリリースである GHC 7.8 (base-4.7) では GHC.TypeLits の内容が大幅に変わっている。一方、それ以降はAPIの非互換な変更はあまり行われていなさそうだ。 ↩

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

GHCの型レベル自然数を理解する

初級編

雰囲気を掴む

使い所

Nat カインド

リテラル

実行時に使える値の取得： KnownNat クラス

中級編

実行時の値を型レベル自然数に持ち上げる

Integer vs Natural

等価性の比較： sameNat

型レベル計算

型レベル計算の限界：自然数の等式

型レベル計算の限界その2：KnownNat のインスタンス

GHCの Nat は帰納的な定義ではない

型レベル計算の限界を克服する

ライブラリーの利用

compiler pluginによる解決

黒魔術編

GHCに型レベル自然数の等価性を納得してもらう

型レベル自然数の演算結果の KnownNat を自前で用意する

応用：型レベル素数判定

関連記事

おまけ：Symbol カインド

追記：Nat 型と Natural 型

`Nat` カインド

実行時に使える値の取得： `KnownNat` クラス

等価性の比較： `sameNat`

型レベル計算の限界その2：`KnownNat` のインスタンス

GHCの `Nat` は帰納的な定義ではない

型レベル自然数の演算結果の `KnownNat` を自前で用意する

おまけ：`Symbol` カインド

追記：`Nat` 型と `Natural` 型