具有种类和类型变量的Haskell多态性

Question

在Haskell中,我了解到类型变量(例如id :: a -> a),应用于类型签名,以及种类(例如Maybe :: * -> *),应用于类型构造函数和类型类.类型必须具有种类*(是具体类型)才能保存值.

我们使用类型变量来启用多态:Nothing :: Maybe a意味着常量Nothing可以属于一系列可能的类型.这使我相信kinding和类型变量具有相同的目的; 最后的代码示例不会像简单的那样工作Nothing :: Maybe,其中类型类可能仍然* -> *表示该类型属于泛型族吗？

我们看起来正在做的是获取一个空参数(* -> *)并用一个a表示相同方差级别的类型变量()填充它.

我们在另一个例子中看到了这种行为

>>> :k Either
Either :: * -> * -> *
>>> :t Left ()
Left () :: Either () b
>>> :t Right ()
Right () :: Either a ()

为什么在理论上有必要区分种类和类型变量？

Answer 1

它们与打字和通常(价值级别)变量截然不同.变量有类型,但它们不是类型.同样,类型变量也有种类.类型变量是主要的概念:没有他们,你没有参数多态,它们还存在于如Java,C#等,但哈斯克尔更进一步在允许类型,其走参数(许多其他语言[],Maybe,->等.)独立存在并具有代表这种非具体类型的类型变量.这意味着它需要一种类型的系统来禁止这样的事情Maybe Int Int.

从示例中,您似乎建议您可以编写没有类型变量的签名,并将其恢复为签名.但后来你怎么能区分a -> b -> a和a -> b -> b？