GHC.TypeLits
Nat kindやKnownNat型クラスを中心としたmodule
hackage
usecases
要素数を保持するVector型
行列計算 ref
ServantのStatus Codeの定義に使われているref
GHC.TypeNats
someNatVal :: Integer -> Maybe SomeNat
code: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の解説