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

【问题标题】：Haskell Polymorphism With Kinds and Type Variables具有种类和类型变量的 Haskell 多态性
【发布时间】：2016-08-25 03:17:52
【问题描述】：

在 Haskell 中，我了解到有应用于类型签名的 类型变量（例如 id :: a -> a）和种类（例如 Maybe :: * -> *），适用于类型构造函数和类型类。一个类型必须有 kind *（是一个具体类型）才能保存值。

我们使用类型变量来启用多态性：Nothing :: Maybe a 表示常量Nothing 可以属于一系列可能的类型。这使我相信 kinding 和 type 变量具有相同的目的。最后一个代码示例不会像Nothing :: Maybe 一样简单地工作，其中类型类Maybe 仍然使用* -> * 来表示该类型属于泛型家族？

我们所做的似乎是采用一个空参数 (* -> *) 并用代表相同方差水平的类型变量 (a) 填充它。

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

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

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

【问题讨论】：

It's not
@bheklilr 我认为 OP 有一些不同的想法，虽然我不太明白。
如果你启用PartialTypeSignatures，你可以用_代替类型变量。例如，Nothing :: Maybe _ 或 Left () :: Either _ _。您提出的将是一个简单的句法扩展，但我不确定它不会带来更多的混乱（尤其是在 PolyKinds 等其他扩展的上下文中）

标签： haskell polymorphism

【解决方案1】：

它们是不同的，就像打字一样，通常（值级）变量是不同的。变量有类型，但它们不是类型。同样，类型变量有种。类型变量是主要概念：没有它们你就没有参数多态性，它们也存在于许多其他语言中，如 Java、C# 等。但 Haskell 更进一步允许使用 types-which-take-parameters ([], Maybe、-> 等）独立存在并具有表示此类非具体类型的类型变量。这意味着它需要一个友好的系统来禁止像Maybe Int Int 这样的事情。

从示例中，您似乎建议您可以编写没有类型变量的签名并将其恢复为带有它们的签名。但是你怎么能区分a -> b -> a和a -> b -> b呢？

【讨论】：

可以将类型和种类混合在一起。事实上，最新的 ghc 有一个语言扩展。但是，必须非常小心地处理被视为逻辑类型的类型，以避免不一致。但这对 Haskell 来说并不重要。