haskell - RankNType 内的约束

Question

下面的函数不进行类型检查。

test1 :: forall x. (Show x => x) -> String
test1 = show

这是因为最后一个->无权访问该约束。 (这可能不是正确的术语，但希望它有意义。)我一直在尝试寻找类似于上面的类型签名的用途，其中最终 ->无权访问该约束。但我想不出任何例子。

所以我的问题是:是否存在这样的情况:我们在类型签名中设置最终 -> 的约束是有用的。无权访问？

<小时/>

请注意 test1与下面的 2 阶函数不同。

test2 :: (forall x. Show x => x) -> String
test2 = show

我对第一个案例感兴趣，而不是这个案例。原因RankNTypes标题中是因为需要启用该扩展才能为 test1 创建类型签名.

Answer 1

将类约束视为推断的函数参数很有用，因为它们对 GHC Core 中的函数和函数应用程序进行了脱糖处理。

让我们对有问题的类型进行脱糖:

newtype ShowDict a = ShowDict (a -> String)
test1 :: forall x. (ShowDict x -> x) -> String

或更简单地说:

test1 :: forall x. ((x -> String) -> x) -> String

这种类型并不是很有用。根据参数性，它的实现必须是返回某个字符串的常量函数。

对于原始的非脱糖类型，我们甚至无法使用 (Show x => x) 参数执行任何操作，因为没有任何 Show我们普遍量化的x的字典。

So my question is: Is there ever a case where we it's useful to have constraints in a type signature that the final -> doesn't have access to?

这有点含糊不清，但我可以争论以下几点:函数参数类型的形式为 (c x => t) (其中 x 可能以外部作用域)在 Haskell 中没有任何意义。

类一致性意味着每种类型至多有一个实例，因此对 c x 进行抽象不会产生任何计算差异。如果没有c x，那么(脱糖的)函数永远无法应用，但如果我们已经知道有一个唯一的c x，那为什么还要依赖它呢？