【2020年4月20日追記】GHCの型レベル自然数については、より網羅的な記事を書いた。型レベル自然数についてより詳しく知りたい方は、こちらの記事も参照いただきたい：GHCの型レベル自然数を理解する【追記終わり】

最近のGHCでは、自然数をパラメーターとするデータ型を定義できる。固定長リストの長さを型に持たせるとか、行列の大きさを型に持たせるとか、そういうことができる。あるいは、自然数 m に対して Z/mZ を表す型を作ることもできる。m を素数とすればこれは有限体となる。

実際に、型レベル自然数を使って Z/mZ に相当する型を作ってみよう。（名前は FiniteField とした）

GHC の DataKinds 拡張により型レベル自然数が使えるようになる。KindSignatures 拡張は、 FiniteField 型のパラメーター p のカインドを p :: Nat と明示するために使っている。

FiniteField p 型は、整数を p で割った余りを保持している。

mkFF 関数では、整数の mod p での剰余を計算して FiniteField p の値を作る。この時、型レベル自然数から実行時に使える値を取り出す必要がある。

型レベル自然数から実行時に使える値を取り出すには、 GHC.TypeLits モジュールにある natVal :: forall n proxy. KnownNat n => proxy n -> Integer が使える。proxy を FiniteField としたものを characteristic 関数としている。

mkFF 関数で natVal 関数または characteristic 関数を使うには、 FiniteField p 型または Proxy p 型の値を渡す必要があるが、Haskell では関数の型宣言で使った型変数を別の場所で使うことはできない、つまり

mkFF :: KnownNat p => Integer -> FiniteField p
mkFF n = MkFF (n `mod` natVal (Proxy :: Proxy p))

と書くことはできない。仕方ないので、関数が返すべき値を変数で受けてそれを characteristic 関数に渡している。ちなみに、 ScopedTypeVariables 拡張を有効にすれば、関数の型宣言で使う型変数を forall で明示的に量化した場合に関数の内部でも使えるようになる。つまり

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Proxy

mkFF :: forall p. KnownNat p => Integer -> FiniteField p
mkFF n = MkFF (n `mod` natVal (Proxy :: Proxy p))

という風に書ける。

recip 関数の実装は手抜きしている。

Num クラスの abs, signum 関数と Fractional クラスの fromRational 関数については、以前の記事に書いた通り。

この FiniteField 型を使って、

main = print (3 / 7 :: FiniteField 11)

と書けば実行時に 2 が出力される。

実行時の値を使う

これで、有限体を使った計算ができるようになった。しかし、標数はプログラム中に直接書き込まなくてはならないのだろうか。標数が実行時に決まるプログラム、例えば、標数をコマンドライン引数で与える有限体電卓は作れないのだろうか。

C++ のテンプレートだとテンプレート引数はコンパイル時に確定している必要があるのでそういうことはできないが、 Haskell の多相は C++ とは実現方法が違うので、（黒魔術を駆使して）頑張ればできないことはなさそうである。

結論を言うと、reflection パッケージの Data.Reflection を使えば実行時の値を型レベル自然数として使うことができる。具体的には、

someCalculation :: KnownNat p => Proxy p -> IO ()

という関数があった時に

do m <- (readIO 等)
   reifyNat m someCalculation

とすると、someCalculation 関数の型パラメーター p として実行時の値 m を与えることができる。

詳しい原理については、マニュアルに論文へのリンクが貼ってあるので、それを参照するべし。ただし、実際の Data.Reflection の実装では、 GHC における型クラスの実現方法（辞書渡し）を悪用した黒魔術を使っているらしい。

【2020年4月16日 追記】「実行時の値を基にした型レベル自然数を作る」こと自体はData.Reflectionを使わなくてもGHC.TypeLitsの型と関数だけで可能だった。具体的には存在型 SomeNat と someNatVal 関数を使って

do m <- (readIO 等)
   case someNatVal m of
     Just (SomeNat proxy) -> someCalculation proxy
     Nothing -> error "negative integer"

とすればよい。また、GHC.TypeLits では型レベル自然数の実行時の型が Integer として扱われるが、GHC 8.2 以降にある GHC.TypeNats を使うと型レベル自然数の値を Natural 型として扱うことができる（natValの返り値の型や someNatVal の引数の型が Natural になる）。【追記終わり】

例として、コマンドライン引数（省略された場合は 11）で与えられた数を標数とする体（素数じゃない値を弾いているわけではないので体になるとは限らないが）で 3 / 7 を計算するプログラム：

Proxy p 型から FiniteField p 型を得るために asFiniteField という関数を用意して使っているが、ScopedTypeVariables 拡張を有効にすれば

someCalculation :: forall p. KnownNat p => Proxy p -> IO ()
someCalculation proxy = print (3 / 7 :: FiniteField p)

と書ける。

ここで使っている isPrime 関数の実装が手抜きなのは言うまでもない。