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

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

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

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

# 初級編

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

## 雰囲気を掴む

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

```haskell
{-# 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` であり[^type-kind]、 `Maybe` や `IO` のような「型を受け取る型構築子」のカインドは `Type -> Type` である。これに対し、型レベル自然数のカインドは `Nat` である。

[^type-kind]: 以前は「普通の型」のカインドは `*` と表記されていたが、型とカインドが統合される流れの中で `*` は型演算子と紛らわしいので、普通の型のカインドとしては `Data.Kind` モジュールの `Type` を使う方が良さそうだ。

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

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

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

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

[^standalonekindsignatures]: GHC 8.10 以降では `StandaloneKindSignatures` 拡張で `type IntMod :: Nat -> Type; newtype IntMod m = ...` と書くこともできる。

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

```haskell
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` カインドの型変数を使う関数を定義しても、関数の処理の中でそれを使うことはできない。

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

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

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

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

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

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

```haskell: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` である。

```haskell
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` のインスタンスを実行時に作り出すための型と関数が用意されている。それがこれだ：

```haskell: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` 型を入手できた場合の使い方も見ておこう。一番簡単な、「型レベル自然数の値を表示する」コードは次のようになる：

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

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

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

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

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

```haskell
{-# 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を使っている。

```haskell:Data.Reflection
reifyNat :: forall r. Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r
```

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

[^ghc8.2-reifyNat]: GHC 8.2では実際に `KnownNat` の内部表現が変わり、reflectionパッケージの `reifyNat` が誤動作をしていた（[当該issue](https://github.com/ekmett/reflection/issues/41)）。reflectionパッケージの最新リリース (2.1.5) では修正済み。

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

[^ghc-typelits-stability]: `GHC.TypeLits` 登場当初の GHC 7.6 (base-4.6) と次のリリースである GHC 7.8 (base-4.7) では `GHC.TypeLits` の内容が大幅に変わっている。一方、それ以降はAPIの非互換な変更はあまり行われていなさそうだ。

まあ、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 以降でも動く。

```haskell: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` を返す」関数を定義してみよう。

```haskell
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` で値を取得して普通に `==` で比較することだろう。

```haskell
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` に包んで返す。

```haskell: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` は同じ型として扱われる。

```haskell:Data.Type.Equality
data a :~: b where
  Refl :: a :~: a
```

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

```haskell
-- 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` 拡張を有効にする。

```haskell
{-# 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` で提供されている型レベル関数（演算子）は、次の通りである。

```haskell: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
```

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

```haskell
{-# 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) -- コンパイルが通る
```

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

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

```haskell
{-# 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)) -- コンパイルが通る
```

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

```haskell
{-# 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` が同じ型であることはわからないのだ。

先の例

```haskell
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](https://downloads.haskell.org/~ghc/7.8.1/docs/html/users_guide/release-7-8-1.html)

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

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

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

```haskell
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` ではなく、独自に型レベル自然数を定義すれば、この手の問題は発生しない。例えば、ペアノ流に自然数を

```haskell
data Nat = Z | S Nat

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

と定義するというやり方が考えられる。実際、[finパッケージ](https://hackage.haskell.org/package/fin)ではそのように定義された `Nat` 型（カインド）を提供している。

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

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

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

デメリットは、

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

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

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

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

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

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

## ライブラリーの利用

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

まず、Haskellコードで

```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 パッケージが提供している）。

```haskell: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パッケージは例えば次のような関数を用意している。

```haskell: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)` が得られるわけだ。使用例は次のようになる：

```haskell
{-# 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` カインドに特化させた場合の型をいくつか紹介しておく。

```haskell: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
```

```haskell: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 からの再エクスポートがいくつかある
```

```haskell: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
```

```haskell:Data.Singletons.Prelude.Ord
sCompare :: SNat x -> SNat y -> SOrdering (CmpNat x y)
```

型演算の結果に対する `KnownNat` が欲しいけどsingletonsは大掛かりすぎる、という場合には、もう少し小さいライブラリとして [typelits-witnesses](http://hackage.haskell.org/package/typelits-witnesses) があるようだ。

## compiler pluginによる解決

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

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

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

```haskell
{-# 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](https://hackage.haskell.org/package/ghc-typelits-extra))。

# 黒魔術編

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

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

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

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

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

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

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

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

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

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

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

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

```haskell
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` にならない」という問題を自前で解決することを考える。方針は

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

となる。

```haskell
-- 要 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) が同じ型だと思い込ませる
```

## 応用：型レベル素数判定

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

```haskell
{-# 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では真っ当な方法では不可能だ。

```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` を利用する。

```haskell
-- 素数判定（手抜き）
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](https://qiita.com/myuon_myon/items/dc6184f8e3d06ce3126c) (2014年10月)
* @mod_poppo, [Haskell (GHC) の型レベル自然数とリフレクションを試してみる](https://blog.miz-ar.info/2016/10/haskell-type-level-naturals-and-reflection/) (2016年10月)
* @autotaker1984, [コンパイル時に素数判定を行ってみた](https://qiita.com/autotaker1984/items/f5cc8914e051563a86f9) (2019年3月)
* @masahiro_sakai, [テンソル形状のコンパイル時検査＋実行時アサーション化を今のHaskellで書いてみる](https://qiita.com/masahiro_sakai/items/c48c688d1b8d47d2a5f1) (2019年10月)
* @YoshikuniJujo, [GHCのタイプチェックプラグインについて、すこし](https://qiita.com/YoshikuniJujo/items/f38078d1380c2a31ff3a) (2019年10月)

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

* [#4385: Type-level natural numbers · Issues · Glasgow Haskell Compiler / GHC · GitLab](https://gitlab.haskell.org/ghc/ghc/issues/4385)
* [type nats · Wiki · Glasgow Haskell Compiler / GHC · GitLab](https://gitlab.haskell.org/ghc/ghc/-/wikis/type-nats)

# おまけ：`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` カインド」という言い方をしてきたが、[ドキュメント](https://hackage.haskell.org/package/base-4.14.0.0/docs/GHC-TypeNats.html)を見ると `data Nat` と書かれている。実は、GHC的には `Nat` はあくまで「型」で、それをDataKinds拡張で持ち上げたものが `Nat` カインド、という扱いなのだ。とはいえ、 `Nat` 型は停止する値を持たないので、普通の型としては使いどころがない。

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

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

* [Unification of Nat and Naturals (!3583) · Merge Requests · Glasgow Haskell Compiler / GHC · GitLab](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583)
* [Unify `Nat` and `Natural` by goldfirere · Pull Request #364 · ghc-proposals/ghc-proposals](https://github.com/ghc-proposals/ghc-proposals/pull/364)
* [ghc-proposals/0364-unify-natural.rst at master · ghc-proposals/ghc-proposals](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0364-unify-natural.rst)