如何阅读这个奇怪的类型签名foo :: Sing n - >(KnownNat n => r) - > r

Question

在单例包中,函数withKnownNat具有以下奇怪的类型签名:

withKnownNat :: Sing n -> (KnownNat n => r) -> r.

所述KnownNat n =>上下文是不是后::(hasType)符号,但在第二个函数参数:-> (KnownNat n => r) ->.

我如何阅读此签名？它究竟意味着什么？它在哪里记录？

Answer 1

这两个签名的区别：

withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat' :: KnownNat n => Sing n -> r -> r

是谁需要提供约束KnownNat n成立的证据。

前面带有约束的假设版本（“在::(hasType) 符号之后”）要求 的调用者withKnownNat'能够证明才能KnownNat n调用该函数。该类型签名可以理解为“如果您可以证明KnownNat n，并给我 aSing n和 an r，我将还给您 an r”。

这并不是特别有用，因为它可以通过简单地忽略KnownNat n约束和Sing n参数并仅返回r其给定值来实现。在不知道r是什么的情况下，它实际上无法做太多其他事情来返回r; 它可能会n在某些情况下执行一些操作并引发错误，或者在内部使用不安全的函数进行一些令人讨厌的黑客攻击，但仅此而已。

在实际版本中，并非整个withKnownNat函数受到KnownNat n约束，而是其参数之一具有该约束。这意味着 的调用者withKnownNat 不必能够证明KnownNat n；相反，调用者可以传递需要证明的参数KnownNat n。作为函数的参数¹ ，该类型可以被理解为“在假设成立的情况下KnownNat n => r属于类型的值”。因此，整个签名可以理解为“如果你给我 (1) a和 (2) 一个在假设成立的情况下属于类型的值，那么我会给你一个类型的值”。r KnownNat nSing nrKnownNat nr

仅仅从类型上我们就可以看出这要有用得多。由于它在 中是多态的，因此获得 an 的r唯一方法是从我们给它的 中获取。它只有在能够证明的情况下才能实际使用该值作为类型的值返回给我们。所以基本上这种类型的 for相当于一个承诺，只要我们有 a ，我们也可以使用任何需要它的东西；正是我们必须调用的方法才能将一种转换为另一种。withKnownNatrKnownNat n => rKnownNat n => rrKnownNat nwithKnownNatSing nKnownNat nnwithKnownNat

¹这与函数的返回值含义相同，但事实证明，获取需要约束的返回值与整个函数需要约束的结果完全相同，因此 GHC 始终会转换类型喜欢arg -> (constraints => result)只是constraints => args -> result。