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

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

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

id :: a -> a

那是多态的。您可以替换a := Int并获取Int -> Int，a := Float -> Float然后获取(Float -> Float) -> Float -> Float。但是，你不能说a := Maybe和得到id :: Maybe -> Maybe。那是没有意义的。相反，我们必须要求您只能替换像Int和Maybe Floatfor这样的具体类型a，而不是像这样的抽象类型Maybe。这是使用 kind 系统处理的。这对你的问题不太重要，所以我只是总结一下。IntandFloat和Maybe Float都是具体的类型（也就是说，它们有值），所以我们说它们有类型Type（类型的类型通常称为它的种类）。Maybe是一个函数，它接受一个具体类型作为参数并返回一个新的具体类型，所以我们说Maybe :: Type -> Type. 在类型a -> a，我们说类型变量a必须有 type 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, and also id :: Float -> Float, and also id :: (Int -> Int) -> Int -> Int, ad infinitum, 同时。这个无限的类型家族可以用一种多态类型来概括，id :: a -> a. 这种观点为您提供了Hindley-Milner 类型系统。这不是现代 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是一个接受两个参数的函数。第一个参数是 a Type，命名为a。第二个参数是一个a. 结果也是一个a。类型签名是：

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

forall基本上是一种新的功能箭头。请注意，它为a. 在 HM 中，当我们说时id :: a -> a，我们并没有真正定义什么a 是。这是一个新鲜的全局变量。按照惯例，最重要的是，该变量不会在其他任何地方使用（否则Gen迭代规则不适用，一切都会崩溃）。如果我后来写了 eg inject :: a -> Maybe a，文本中出现的a将是指一个新的全局实体，不同于id. 在 System F 中，ainforall a. a -> a实际上有作用域。它是一个“局部变量”，只能在forall. ain可能是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 中，如果某事物具有多态类型，那么它同时也具有无穷多的单态类型。在 System F 中，一个事物只能有一种类型。有类型，不是或。为了摆脱，您必须实际给它一个参数：和。id = /\a -> \(x :: a) -> xforall a. a -> aInt -> IntFloat -> FloatInt -> Intidid Int :: Int -> Intid Float :: Float -> Float

然而，Haskell 不是 System F。System F 更接近 GHC 所称的 Core，它是 GHC 将 Haskell 编译成的内部语言——基本上没有任何语法糖的 Haskell。Haskell是基于 System F 核心的 Hindley-Milner 风格的单板。在 Haskell 中，名义上多态类型是一种类型。它们不像类型的集合。但是，多态类型仍然是第二类。Haskell 不允许你在forall没有-XExplicitForalls. forall它通过在某些地方插入 s 来模拟 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)- 你必须定义 egnewtype Bool = Bool { ifThenElse :: forall a. a -> a -> a }将多态性包装在单态的东西下。除非您启用，否则您不能显式给出类型参数-XTypeApplications，然后您可以编写id @Int :: Int -> Int. 你不能写类型 lambdas ( /\), period ; 相反，它们会尽可能隐式插入。如果你定义id :: forall a. a -> a，那么你甚至不能id用 Haskell 编写。它将始终隐式扩展为应用程序，id @_.

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

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

问题描述

解决方案

推荐阅读