generated at
GHC.TypeLits
Nat kindやKnownNat型クラスを中心としたmodule

hackage

usecases
要素数を保持するVector型
行列計算 ref
ServantのStatus Codeの定義に使われているref



GHC.TypeNats


someNatVal :: Integer -> Maybe SomeNat
hs
-- GHC.TypeNats data SomeNat = forall n. KnownNat n => SomeNat (Proxy n) -- GHC.TypeLits someNatVal :: Integer -> Maybe N.SomeNat someNatVal n | n >= 0 = Just (N.someNatVal (fromInteger n)) | otherwise = Nothing
KnownNat型クラスのinstanceを実行時に作る
つまり、入力された自然数のデータを安全に型レベル自然数に変換できる




参考
GHCの型レベル自然数を理解する - Qiita
良すぎる

>#WIP


https://qiita.com/mod_poppo/items/3a37424d299a9f71b757#中級編
この辺から読む
https://haskell.e-bigmoon.com/posts/2019/09-09-extensible-ast.html
https://a-kawashiro.hatenablog.com/entry/2016/12/06/212431
https://scrapbox.io/haskell-shoen/GHC.TypeLits
https://blog.miz-ar.info/2016/10/haskell-type-level-naturals-and-reflection/
https://qiita.com/myuon_myon/items/dc6184f8e3d06ce3126c
https://hackage.haskell.org/package/base-4.15.0.0/docs/GHC-TypeLits.html#v:someNatVal
https://qiita.com/aiya000/items/6e6946b2604fcaf621bb#ghctypelits-

https://kowainik.github.io/posts/membrain
若干関係ないかもしれないが
Kowainikのmembrainというpackageの解説