10

当我声明这个新类型时：

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处理这种情况？

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

4

2 回答 2

12

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

从我想将一流的多态函数传递给 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

推理禁用错误检测

ifr是作为 的参数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可以绑定。

于 2018-01-12T13:46:20.667 回答
4

关键是构造函数不会有你提到的 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。

于 2018-01-12T13:08:21.420 回答