haskell - 了解 `GHC.TypeLits`

Question

我正试图围绕 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 - 类型级别编号怎么可能是未知的？ 不是类型级别编号的全部意义吗？是 在编译时知道吗？

Answer 1

这个问题很宽泛——我只谈几点。
proxy类型变量只是一种类型变量 * -> * ，即类型构造函数的类型。务实地说，如果你有一个功能

foo :: proxy a -> ...

您可以将类型的值传递给它，例如 Maybe Int , 选择 proxy = Maybe和 a = Int .您还可以传递 [] Char 类型的值(也写为 [Char] )。或者，更常见的是 Proxy Int 类型的值, 其中 Proxy是一种数据类型，定义为

data Proxy a = Proxy

即不携带任何运行时信息的数据类型(它只有一个值!)，但携带编译时信息(幻像类型变量 a )。

假设 N是一种类型 Nat -- 编译时自然。我们可以写一个函数

bar :: N -> ...

但是调用它需要我们建立一个 N 类型的值。 ——这无关紧要。类型 N 的用途只是携带编译时信息，它的运行时值并不是我们真正想要使用的东西。事实上， N除了底部之外，可能根本没有任何值。我们可以打电话

bar (undefined :: N)

但这看起来很奇怪。读到这里，我们必须意识到 bar它的第一个论点是懒惰的，并且尝试使用它不会引起分歧。问题是 bar :: N -> ...类型签名具有误导性:它声称结果可能取决于类型 N 的参数的值, 当情况并非如此时。相反，如果我们使用

baz :: Proxy N -> ...

意图很明确——只有一个运行时值: Proxy :: Proxy N .同样清楚的是 N value 仅在编译时存在。

有时，而不是使用特定的 Proxy N , 代码稍微概括为

foo :: proxy N -> ...

它实现了相同的目标，但也允许不同的 Proxy类型。 (就个人而言，我对这种概括并不感到非常兴奋。)

回到问题: natVal是一个函数，它可以将编译时自然地转换为运行时值。 IE。它转换 Proxy N进入 Int ，只返回常数。

如果您使用类型模板参数来模拟编译时自然值，您与 C++ 模板的类比可能会更接近。例如。

template <typename N> struct S { using pred = N; };
struct Z {};

template <typename N> int natVal();
template <typename N> int natVal() { return 1 + natVal<typename N::pred>(); }
template <>           int natVal<Z>() { return 0; }

int main() {
    cout << natVal<S<S<Z>>>() << endl;  // outputs 2
    return 0;
}

假设 S 没有公共(public)构造函数和 Z :它们的运行时值并不重要，只有它们的编译时信息才重要。