为什么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

这是编程语言设计的问题.它可以用你建议的方式推断,但我认为这是一个坏主意.

从类型签名中我不想将第一类多态函数传递给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两个字段中的变量实际上不在同一个活页夹下,但它看起来一目了然.

与类似结构的比较

请注意类似于您建议的类型类,可以看作是一种记录:

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可以约束.