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

Question

在 singletons 包中，函数 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 ，并给我一个 Sing n 和一个 r ，我将还给你一个 r ”。

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

在实际版本中，它不是完整的withKnownNat KnownNat n 下的函数约束，而是它的参数之一具有该约束。这意味着 withKnownNat 的调用者不需要必须能够证明KnownNat n ;相反，调用者可以传递一个需要 KnownNat n 证明的参数。 。作为类型 KnownNat n => r 的函数的参数¹可以理解为“在 r 成立的假设下，KnownNat n 类型的值”。因此，整个签名可以理解为“如果你给我(1)一个 Sing n 和(2)一个类型为 r 的值，并且假设 KnownNat n 成立，那么我会给你类型为 r "的值。

仅从类型上我们就可以看出这要有用得多。因为它是多态的 r ，唯一的办法withKnownNat可以获得 r来自KnownNat n => r我们给了它。它实际上只能使用 KnownNat n => r值作为 r 类型的值如果可以证明 KnownNat n 就返回给我们 。所以基本上这种类型为 withKnownNat相当于一个 promise ，每当我们有 Sing n ，我们还可以使用任何需要 KnownNat n 的东西同样n ; withKnownNat这正是我们必须调用的将一种转换为另一种的方法。

<小时/>

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