haskell - 为什么 rank-n 类型需要显式的 forall 量词？

Question

当我声明这个新类型时:

newtype ListScott a = 
  ListScott { 
  unconsScott :: (a -> ListScott a -> r) -> r -> r 
}

这将定义假设的 rank-2 类型 ListScott :: ((a -> ListScott a -> r) -> r -> r) -> ListScott a ，编译器提示 r不在范围内。从类型签名中我想将一流的多态函数传递给 ListScott 不是很明显吗？ ?

为什么 r 需要显式类型限定符对于这样的情况？

我不是类型理论家，可能忽略了一些东西......

Answer 1

这是编程语言设计的问题。可以按照您建议的方式推断，但我认为这是一个坏主意。

Isn't it apparent from the type signature that I want to pass a first class polymorphic function to ListScott?

我不认为我们可以从这个定义中明显看出那么多。

普遍的还是存在的？与 GADT 表示法冲突

这是我们可以用 GADTs 写的东西扩大:

data ListScott a where
  ListScott :: { unconsScott :: (a -> ListScott a -> r) -> r -> r } -> ListScott a

这里 r在 unconsScott 中存在量化字段，因此构造函数具有以下第一种类型:

ListScott :: forall a r. ((a -> ListScott a -> r) -> r -> r) -> ListScott a
-- as opposed to
ListScott :: forall a. (forall r. (a -> ListScott a -> r) -> r -> r) -> ListScott a

推理禁用错误检测

如果 r而是作为 ListScott 的参数，但我们只是忘了添加它？我认为这是一个合理可能的错误，因为假设 ListScott r a和 ListScott a可以在某些方面作为列表的表示。然后，绑定(bind)器的推断将导致错误的类型定义被接受，并且一旦类型被使用，错误就会在其他地方报告(希望不会太远，但这仍然比定义本身的错误更糟糕)。

显式性还可以防止类型构造函数被错误输入为类型变量的拼写错误:

newtype T = T { unT :: maybe int }
-- unlikely to intentionally mean "forall maybe int. maybe int"

仅在类型声明中没有足够的上下文来自信地猜测变量的含义，因此我们应该强制正确绑定(bind)变量。

可读性

考虑函数记录:

data R a = R
  { f :: (r -> r) -> r -> r
  , g :: r -> r
  }

data R r a = R
  { f :: (r -> r) -> r -> r
  , g :: r -> r
  }

我们必须看向 = 的左侧确定是否 r绑定(bind)在那里，如果不是，我们必须在每个字段中插入活页夹。我发现这使得第一个版本难以阅读，因为 r这两个字段中的变量实际上不会在同一个活页夹下，但一目了然。

与类似结构的比较

请注意，类型类会发生与您建议的类似的事情，这可以看作是一种记录:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

上面的大多数论点也适用，因此我更愿意将该类写为:

class Functor f where
  fmap :: forall a b. (a -> b) -> f a -> f b

本地类型注释也可以这样说。但是，顶级签名不同:

id :: a -> a

这明确意味着 id :: forall a. a -> a , 因为没有其他级别 a可以绑定(bind)。