在GHC.TypeLits中,someNatVal的优点是什么(我们用natVal无法实现)？

Question

我正在努力理解GHC.TypeLits,特别是someNatVal.我理解它在这个博客使用的方式张贴在这里,但提到同样的例子也一直在使用中实现natVal,如:

isLength :: forall len a. KnownNat len => Integer -> List len a -> Bool
isLength n _ = n == natVal (Proxy :: Proxy len)

是否有任何用途someNatVal不能改写natVal？

Answer 1

主要用途someNatVal是在运行时使用一个值，就好像它是编译时未知的类型一样。

我对“我可以有一个未知的 KnownNat 吗？”的回答 提供了一个非常愚蠢的例子。有一百万种更好的方法来编写与该程序执行相同操作的程序。但它显示了什么someNatVal。它本质上是一个从值到类型的函数 - 存在将该类型的范围限制在静态未知的地方。