在单例包中，函数withKnownNat具有以下奇怪的类型签名:withKnownNat :: Sing n -> (KnownNat n => r) -> r。KnownNat n =>上下文不在::(hasType)符号之后，而是在第二个函数参数-> (KnownNat n => r) ->中。
如何阅读此签名？这到底是什么意思？它在哪里记录？
最佳答案
这两个签名之间的区别:
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat' :: KnownNat n => Sing n -> r -> r
是谁需要提供证明
KnownNat n成立的证据。前面具有约束条件的假设版本(“
::(hasType)符号之后”)要求withKnownNat'的调用者能够证明KnownNat n才能调用该函数。可以将这种类型签名读作类似“如果您可以证明KnownNat n，并同时给我Sing n和r，我会还给您r”。这并不是特别有用，因为可以通过简单地忽略
KnownNat n约束和Sing n参数并仅返回给定的r来实现。而且不知道r是什么，返回r并不能做很多其他的事情;它可能会使用n进行某些操作，并在某些情况下引发错误，或者在内部使用不安全的功能进行讨厌的黑客入侵，仅此而已。在实际版本中，不是整个
withKnownNat函数都受KnownNat n约束，而是其参数之一具有该约束。这意味着withKnownNat的调用者不必证明KnownNat n；相反，调用者可以传递需要KnownNat n证明的参数。作为函数的自变量1，可以将KnownNat n => r类型读取为“在假定r成立的情况下，类型为KnownNat n的值”。因此，整个签名可以理解为“如果在假设Sing n成立的情况下，如果同时给我(1)r和(2)一个KnownNat n类型的值，那么我将给您一个r类型的值” 。我们可以看到，仅从类型上来看，这是有用的。由于它在
r中是多态的，所以withKnownNat可以获取r的唯一方法是从我们给它的KnownNat n => r中获取。如果可以证明KnownNat n => r，它只能实际使用r值作为KnownNat n类型的值返回给我们。因此，基本上，这种类型的withKnownNat意味着可以保证，只要我们有Sing n，我们就可以为同一个KnownNat n使用需要n的任何内容； withKnownNat只是我们将一个转换为另一个的调用。1它也与函数的返回值具有相同的含义，但是事实证明，获得需要约束的返回值与整个函数需要约束的结果完全相同，因此GHC总是转换类型就像
arg -> (constraints => result)到constraints => args -> result一样。