哪个是多态类型：一个类型还是一组类型？

Question

Hutton 在 Haskell 中编程说：

包含一个或多个类型变量的类型称为多态。

什么是多态类型：一个类型还是一组类型？

具有具体类型替换其类型变量的多态类型是类型吗？

具有不同具体类型替换其类型变量的多态类型被视为相同类型还是不同类型？

Answer 1

具有具体类型替换其类型变量的多态类型是类型吗？

这就是重点，是的。但是，您需要小心。考虑：

id :: a -> a

这是多态的。您可以替换a := Int 并得到Int -> Int 和a := Float -> Float 并得到(Float -> Float) -> Float -> Float。但是，您不能说a := Maybe 并得到id :: Maybe -> Maybe。那是没有意义的。相反，我们必须要求您只能将Int 和Maybe Float 之类的具体类型替换为a，而不是Maybe 之类的抽象类型。这是使用 kind 系统处理的。这对你的问题不太重要，所以我只是总结一下。 Int 和 Float 和 Maybe Float 都是具体类型（即它们有值），所以我们说它们有类型 Type （类型的类型通常称为它的种类）。 Maybe 是一个函数，它接受一个具体类型作为参数并返回一个新的具体类型，所以我们说Maybe :: Type -> Type。在a -> a 类型中，我们说类型变量a 必须具有Type 类型，所以现在允许替换a := Int、a := String 等，而诸如a := Maybe 之类的内容则不允许。

具有不同具体类型替换其类型变量的多态类型被认为是相同类型还是不同类型？

没有。回到a -> a：a := Int 给出Int -> Int，但a := Float 给出Float -> Float。不一样。

什么是多态类型：一个类型还是一组类型？

现在这是一个加载的问题。你可以跳到最后的 TL;DR，但是“什么是多态类型”这个问题实际上在 Haskell 中确实令人困惑，所以这里是一堵文字墙。

有两种查看方式。 Haskell 从一个开始，然后转到另一个，现在我们有大量的旧文献提到旧方式，因此现代系统的语法试图保持兼容性。这有点混乱。考虑

id x = x

id 的类型是什么？一种观点是id :: Int -> Int，还有id :: Float -> Float，还有id :: (Int -> Int) -> Int -> Int，无限同时。这个无限的类型家族可以用一种多态类型来概括，id :: a -> a。这个观点给你Hindley-Milner type system。这不是现代 GHC Haskell 的工作方式，但这个系统是 Haskell 在创建时所基于的。

在 Hindley-Milner 中，多态类型和单态类型之间有一条硬线，这两个组的并集通常为您提供“类型”。说在 HM 中，多态类型（在 HM 行话中，“多型”）是类型并不公平。您不能将多型作为参数，或者从函数中返回它们，或者将它们放在列表中。相反，多型只是单型的模板。如果你眯着眼睛，在 HM 中，多态类型可以看作是一组符合模式的单型。

现代 Haskell 建立在 System F（加上扩展）之上。在系统 F 中，

id = \x -> x -- rewriting the example

不是一个完整的定义。因此我们甚至不能考虑给它一个类型。每个 lambda 绑定变量都需要类型注释，但 x 没有注释。更糟糕的是，我们甚至无法确定一个：\(x :: Int) -> x 和\(x :: Float) -> x 一样好。在 System F 中，我们所做的就是写

id = /\(a :: Type) -> \(x :: a) -> x

使用/\ 表示Λ（大写lambda）就像我们使用\ 表示λ。

id 是一个接受 两个 参数的函数。第一个参数是Type，名为a。第二个参数是a。结果也是a。类型签名是：

id :: forall (a :: Type). a -> a

forall 基本上是一种新的函数箭头。请注意，它为a 提供了一个活页夹。在 HM 中，当我们说 id :: a -> a 时，我们并没有真正定义 a 是什么。这是一个新鲜的全局变量。按照惯例，最重要的是，该变量不会在其他任何地方使用（否则Generalization 规则不适用，一切都会崩溃）。如果我写了例如inject :: a -> Maybe a，之后，a 的文本出现将指代一个新的全局实体，与 id 中的不同。在系统 F 中，forall a. a -> a 中的 a 实际上具有范围。它是一个“局部变量”，只能在 forall 下使用。 inject :: forall a. a -> Maybe a 中的 a 可能是也可能不是“相同的”a；没关系，因为我们有实际的范围规则来防止一切崩溃。

因为 System F 对类型变量有卫生的范围规则，所以允许多态类型做任何其他类型可以做的事情。您可以将它们作为参数

runCont :: forall (a :: Type). (forall (r :: Type). (a -> r) -> r) -> a
runCons a f = f a (id a) -- omitting type signatures; you can fill them in

你把它们放在数据构造函数中

newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b)

您可以将它们放在多态容器中：

type Bool = forall a. a -> a -> a
true, false :: Bool
true a t f = t
false a t f = f

thueMorse :: [Bool]
thueMorse = false : true : true : false : _etc

与 HM 有一个重要的区别。在 HM 中，如果某事物具有多态类型，它也具有，同时，无限单态类型。在 System F 中，事物只能有 one 类型。 id = /\a -> \(x :: a) -> x 的类型为 forall a. a -> a，而不是 Int -> Int 或 Float -> Float。为了从id 中得到Int -> Int，您必须实际给它一个参数：id Int :: Int -> Int 和id Float :: Float -> Float。

但是，Haskell 不是 System F。 System F 更接近 GHC 所称的 Core，它是 GHC 将 Haskell 编译成的内部语言——基本上没有任何语法糖的 Haskell。 Haskell 是在 System F 核心之上的 Hindley-Milner 风格的单板。在 Haskell 中，名义上多态类型是一种类型。它们不像类型的集合。但是，多态类型仍然是第二类。 Haskell 不允许你在没有-XExplicitForalls 的情况下实际输入forall。它通过在某些地方插入foralls 来模拟 Hindley-Milner 的不稳定的隐式全局变量创建。这样做的地方由-XScopedTypeVariables 更改。除非启用-XRankNTypes，否则不能使用多态参数或多态字段。你不能说[forall a. a -> a -> a]，也不能说id (forall a. a -> a -> a) :: (forall a. a -> a -> a) -> (forall a. a -> a -> a)——你必须定义例如newtype Bool = Bool { ifThenElse :: forall a. a -> a -> a } 将多态性包装在单态的东西下。除非启用-XTypeApplications，否则不能显式给出类型参数，然后可以编写id @Int :: Int -> Int。你不能写类型 lambdas (/\)，句号；相反，它们会尽可能隐式插入。如果你定义了id :: forall a. a -> a，那么你甚至不能在Haskell 中写id。它将始终隐式扩展为应用程序id @_。

TL;DR：在 Haskell 中，多态类型是一种类型。它不被视为一组类型，或类型的规则/模式，或其他任何东西。但是，由于历史原因，他们被视为二等公民。默认情况下，如果你稍微眯一下眼，它们看起来只是被视为一组类型。可以通过适当的语言扩展来解除对它们的大多数限制，此时它们看起来更像“只是类型”。剩下的一个很大的限制（不允许进行暗示性实例化）是相当基本的并且无法删除，但这很好，因为有一种解决方法。

Answer 2

这里的“类型”一词有一些细微差别。 值 有具体的类型，不能是多态的。另一方面，表达式具有通用类型，可以是多态的。如果您正在考虑值的类型，那么可以将多态类型松散地视为定义可能的具体类型的集合。 （至少一阶多态类型！高阶多态打破了这种直觉。）但这并不总是一种特别有用的思维方式，也不是一个充分的定义。它没有捕获哪些组类型可以以这种方式描述（以及相关的概念，如参数化。）

不过，这是一个很好的观察，在这两种相关但不同的方式中使用了同一个词“类型”。

Answer 3

编辑：下面的答案原来不能回答这个问题。区别在于术语上的一个细微错误：Maybe 和 [] 等类型是更高种类的，而 forall a. a -> a 和 forall a. Maybe a 等类型是多态。下面的答案与更高种类的类型有关，但问题是关于多态类型的。我仍然保留这个答案，以防它对其他人有所帮助，但我现在意识到这并不是问题的真正答案。

我认为 polymorphic 更高种类的类型更接近于 set 类型。例如，您可以将 Maybe 视为集合 {Maybe Int, Maybe Bool, ...}。

但是，严格来说，这有点误导。为了更详细地解决这个问题，我们需要了解种类。与类型如何描述值类似，我们说种类描述了类型。这个想法是：

• 具体类型（即具有值的类型）有一种*。示例包括Bool、Char、Int 和Maybe String，它们都具有* 类型。这表示为例如Bool :: *。请注意，诸如Int -> String 之类的函数也有类型*，因为它们是可以包含诸如show 之类的值的具体类型！
• 具有类型参数的类型具有包含箭头的种类。例如，与id :: a -> a 一样，我们可以说Maybe :: * -> *，因为Maybe 将具体类型作为参数（例如Int），并生成具体类型作为结果（例如Maybe Int)。像a -> a 这样的东西也有类型* -> *，因为它有一个类型参数（a）并产生一个具体的结果（a -> a）。你也可以得到更复杂的种类：例如，data Foo f x = FooConstr (f x x) 有种类Foo :: (* -> * -> *) -> * -> *。 （你明白为什么吗？）

（如果上面的解释没有意义，Learn You a Haskell 这本书也有a great section on kinds。）

所以现在我们可以正确回答您的问题了：

多态更高种类的类型是一个类型还是一组类型？

两者都不是：多态更高种类的类型是类型级函数，如其种类中的箭头所示。例如，Maybe :: * -> * 是一个类型级函数，它可以转换例如Int → Maybe Int，Bool → Maybe Bool 等

多态更高种类的类型用具体类型替换其类型变量是类型吗？

是的，当你的 polymorphic 更高种类的类型有一种* -> * 时（即它有一个类型参数，它接受一个具体类型）。当您将具体类型 Conc :: * 应用到类型 Poly :: * -> * 时，它只是函数应用程序，如上所述，结果是 Poly Conc :: * 即具体类型。

多态更高种类的类型，用不同的具体类型代替它的类型变量被认为是相同的还是不同的类型？

这个问题有点不合适，因为它与种类没有任何关系。答案肯定是否：Maybe Int 和Maybe Bool 这样的两种类型并不相同。 Nothing 可能是这两种类型的成员，但只有前者包含值Just 4，而只有后者包含值Just False。

另一方面，可能有两个不同的替换，结果类型是同构。 （同构是指两种类型不同，但在某些方面是等价的。例如，(a, b) 和 (b, a) 是同构的，尽管是相同的类型。正式条件是两种类型 @当您可以编写两个反函数p -> q 和q -> p 时，987654366@,q 是同构的。）

Const 就是一个例子：

data Const a b = Const { getConst :: a }

这种类型只是忽略了它的第二个类型参数；因此，Const Int Char 和 Const Int Bool 这样的两种类型是同构的。但是，它们不是同一种类型：如果您创建了 Const Int Char 类型的值，但随后将其用作 Const Int Bool 类型的东西，这将导致类型错误。这种功能非常有用，因为这意味着您可以使用Const a tag“标记”类型a，然后使用tag 作为类型级别信息的标记。