我试图围绕GHC扩展KindSignatures和DataKinds.看看Data.Modular包,我大致了解一下
newtype i `Mod` (n :: Nat) = Mod i deriving (Eq, Ord)
等同于声明一个c ++模板<typename T, int N>(构造函数只接受一个类型的参数T).但是,看看GHC.TypeLits包,我不了解发生的大部分内容.关于这个包的任何一般性解释都会有所帮助.在此问题被标记为非主题之前,这里有一些特定的子问题:
KnownNat类是有意义的,具有所需的功能,让你从类型中提取类型变量,但是做natVal什么,什么是proxy类型变量？someNatVal？SomeNat- 类型级别数如何未知？编译时是否知道类型级别编号的全部内容？这个问题相当广泛——我只谈几点。
类型proxy变量只是 kind 的类型变量* -> *，即类型构造函数的种类。实际上，如果你有一个函数
foo :: proxy a -> ...
您可以将类型值传递给它，例如Maybe Int，选择proxy = Maybe和a = Int。您还可以传递类型的值[] Char（也写为[Char]）。或者，更常见的是 type 的值Proxy Int，其中Proxy数据类型定义为
data Proxy a = Proxy
即不携带任何运行时信息的数据类型（它只有一个值！），但携带编译时信息（幻像类型变量a）。
AssumeN是一种类型Nat——编译时自然的类型。我们可以写一个函数
bar :: N -> ...
但是调用它需要我们构建一个类型的值N——这是无关紧要的。类型的目的N只是携带编译时信息，而它的运行时值并不是我们真正想要使用的东西。事实上，N除了底部之外，可能根本没有任何值。我们可以打电话
bar (undefined :: N)
但这看起来很奇怪。读到这里，我们必须意识到bar它的第一个参数是惰性的，并且尝试使用它不会导致分歧。问题在于bar :: N -> ...类型签名具有误导性：它声称结果可能取决于 type 参数的值N，但事实并非如此。相反，如果我们使用
baz :: Proxy N -> ...
意图很明确——只有一个运行时值：Proxy :: Proxy N。同样清楚的是，该N值仅在编译时存在。
Proxy N有时，代码不是使用特定的，而是稍微概括为
foo :: proxy N -> ...
它实现了相同的目标，但也允许不同的Proxy类型。（就我个人而言，我对这种概括并不感到非常兴奋。）
回到问题：natVal是一个将编译时值自然转换为运行时值的函数。即它转换Proxy N为Int，仅返回常量。
如果您使用类型模板参数来模拟编译时自然数，那么与 C++ 模板的类比可能会更接近。例如
foo :: proxy a -> ...
S假设and没有公共构造函数Z：它们的运行时值并不重要，只有它们的编译时信息很重要。