为什么明确的 forall 量词对于 rank-n 类型是必需的？

Question

当我声明这个新类型时：

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

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

为什么在这种情况下 r 需要显式类型量词？

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

Answer 1

关键是构造函数不会有你提到的 rank-1（是的，一个）类型：（为清楚起见添加了量词）

ListScott1 :: forall a r. ((a -> ListScott a -> r) -> r -> r) -> ListScott a

但是下面的rank-2类型

ListScott2 :: forall a. (forall r. (a -> ListScott a -> r) -> r -> r) -> ListScott a

因此，rank-2 确实参与了您程序的类型检查。

请注意，如果 f :: (Bool -> ListScott Bool -> Char) -> Char -> Char，那么上面的第一个构造函数会使 ListScott1 f :: ListScott Bool 类型良好，但这不是我们想要的。事实上，使用第二个构造函数，ListScott2 f 是错误类型的。

确实，要使 ListScott2 f :: ListScott Bool 类型良好，我们需要一个多态的 f，类型为 f :: forall r. (Bool -> ListScott Bool -> r) -> r -> r.

Answer 2

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

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 都可以在某些方面作为列表的表示。然后绑定器的推断将导致错误的类型定义被接受，并且一旦类型被使用就会在其他地方报告错误（希望不要太远，但这仍然比定义本身的错误更糟糕）。

明确性还可以防止类型构造函数被错误键入为类型变量的拼写错误：

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

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

可读性

考虑功能记录：

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 是否绑定在那里，如果没有，我们必须在每个字段中插入活页夹。我发现这使得第一个版本难以阅读，因为两个字段中的 r 变量实际上不在同一个活页夹下，但一眼看上去肯定是不同的。

与类似构造的比较

请注意，类型 classes 会发生与您所建议的类似的情况，可以将其视为一种记录：

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

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

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

本地类型注释也有类似的情况。但是，顶级签名不同：

id :: a -> a

这明确表示 id :: forall a. a -> a，因为没有其他级别可以绑定 a。

为什么明确的 forall 量词对于 rank-n 类型是必需的？

Why are explicit forall quantifiers necessary for rank-n types?

haskell

types

higher-rank-types

rank-n-types

scott-encoding

普遍的还是存在的？与 GADT 符号冲突

推理禁用错误检测

可读性

与类似构造的比较