这是编程语言设计的问题。可以按照您建议的方式推断,但我认为这是一个坏主意。
从我想将一流的多态函数传递给 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
可以绑定。