KnownNat型クラス

型引数がNat kindであることを明示したいときに使う

定義

code:hs

class KnownNat (n :: Nat) where

natSing :: SNat n

型クラス制約に書けば、mがNat kindであることを要請できる

code:hs

addMod :: KnownNat m => IntMod m -> IntMod m -> IntMod m

addMod t@(IntMod x) (IntMod y) = IntMod ((x + y) mod modulus)

where modulus = natVal t

この時、mはNat kindである

継承させれば、nがNat kindであることを要請できる

code:hs

class KnownNat n => Hoge n where -- nのkindはNat!

...

こっちの例見たことないけどできるはずmrsekut.icon

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

型レベルのnを、値レベルのnに変換する関数

面白みのない例だが、これでイメージは分かると思う

code:hs

{-# LANGUAGE ScopedTypeVariables #-}

newtype N (n :: Nat) = N Int deriving (Eq,Show)

f :: forall n. (KnownNat n) => N n -> Integer

f _ = natVal (Proxy :: Proxy n)

main = do

let a :: N 2

a = N 2

print $ f a -- 2

let b :: N 3

b = N 2

print $ f b -- 3

fは、型レベルのnを見て、natValを経由して値レベルに変換している

bの結果を見たら分かる通り、型と値がズレてたら結果が異なる

fの定義を見れば分かる通り、引数は無視してるので型レベルの方が返される

参考

良すぎる