haskell - 哪个是多态类型 : a type or a set of types?

Question

Hutton 在 Haskell 中编程 说:

A type that contains one or more type variables is called polymorphic.

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

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

用不同的具体类型替换其类型变量的多态类型是相同的还是不同的类型？

Answer 1

Is a polymorphic type with a concrete type substituting its type variable a type?

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

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 这样的东西是允许的不是。

Is a polymorphic type with different concrete types substituting its type variable considered the same or different types?

号返回a -> a :a := Int给 Int -> Int ，但是 a := Float给 Float -> Float .不一样。

Which is a polymorphic type: a type or a set of types?

现在这是一个沉重的问题。你可以跳到最后的 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 行话中，“polytypes”)是类型是不公平的。您不能将多类型作为参数，或者从函数中返回它们，或者将它们放在列表中。相反，多型只是单型的模板。如果你眯着眼睛，在 HM 中，多态类型可以被视为一组符合模式的单类型。

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

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

不是一个完整的定义。因此我们甚至不能考虑给它一个类型。每个 lambda 绑定(bind)变量都需要一个类型注释，但 x没有注释。更糟糕的是，我们甚至无法决定一个:\(x :: Int) -> x和\(x :: Float) -> x一样好.在系统 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曾是。这是一个全新的全局变量。按照惯例，最重要的是，该变量不会在其他任何地方使用(否则 Gen eralization 规则不适用，一切都会崩溃)。如果我写过例如inject :: a -> Maybe a ，之后，文本出现 a将指代一个新的全局实体，与 id 中的实体不同。 .在系统 F 中，a在 forall a. a -> a实际上有范围。它是一个“局部变量”，只能在 forall 下使用。 . a在 inject :: forall a. a -> Maybe 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 中，如果某事物具有多态类型，则它也具有，同时 ，无限的单态类型。在系统 F 中，一个事物只能有一种类型。 id = /\a -> \(x :: a) -> x有类型 forall a. a -> a ，不是 Int -> Int或 Float -> Float .为了得到一个Int -> Int出id ，你必须给它一个参数:id Int :: Int -> Int , 和 id Float :: Float -> Float .

然而，Haskell 不是 System F。 System F 更接近 GHC 所说的 Core，它是 GHC 将 Haskell 编译成的一种内部语言——基本上是 Haskell，没有任何语法糖。 Haskell 是位于 System F 核心之上的 Hindley-Milner flavor 单板。在 Haskell 中，名义上多态类型是一种类型。它们的行为不像类型集。然而，多态类型仍然是二等的。 Haskell 不允许你实际输入 forall没有 -XExplicitForalls .它通过插入 forall 来模拟 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 ，那么你甚至不能写 id在 haskell 。它将始终隐式扩展为应用程序，id @_ .

TL;博士 : 在 Haskell 中，多态类型是一种类型。它不被视为一组类型，或类型的规则/模式，或其他。然而，由于历史原因，他们被视为二等公民。默认情况下，如果您稍微眯一下眼，它们似乎只是被视为类型集。对它们的大多数限制都可以通过合适的语言扩展来解除，此时它们看起来更像是“只是类型”。剩下的一个大限制(不允许使用不可预测的实例化)是相当基本的并且无法删除，但这很好，因为有一种解决方法。