haskell - 在 Haskell 中， "higher-kinded types"*真的*类型吗？或者它们仅仅表示*具体*类型的集合而仅此而已？

Question

参数多态函数

考虑以下函数:

f :: a -> Int
f x = (1 :: Int)

我们可能会说 f 的类型是 a -> Int ，以及f因此是“多态”类型。

以下哪项是最准确的思考方式 f ？

1. 实际上有一个单个f类型 a -> Int 。但是，它可以用作 f :: Int -> Int ，作为f :: Double -> Int等等。

2. 从字面上来说，f的类型不是a -> Int 。事实上，这只是表示存在一个函数 f家族的简写方式。其类型是具体的(即，有 f :: Int -> Int 、 f :: Double -> Double 等等；而且，这些函数中的每一个都彼此不同)。

高等种类

同样，我们可以考虑以下类型声明:

data Maybe a = Just a | Nothing

并询问两种观点哪种更正确:

1. 没有单一类型 Maybe ;事实上，只有一系列具体类型( Maybe Int 、 Maybe String 等)，仅此而已。

2. 事实上只有一种类型 Maybe 。这种类型是高等类型。当我们说它是一种“类型”时，我们指的是字面意思(不是(1)的简写)。正好我们也可以写Maybe Int , Maybe Double等等来生成不同类型(恰好是具体的)。但是，最终(即):Maybe , Maybe Int ，和Maybe String表示三种不同类型，其中两种是具体类型，另一种是高级类型。

问题摘要

在 Haskell 中，“高等类型”真的是类型吗？或者只是具体类型“真实类型”，当我们谈到“更高种类的类型”时，我们仅表示具体类型的家族。此外，参数多态函数是否表示单一类型的函数，或者它们仅表示具体类型的集合函数em>(仅此而已)？

Answer 1

目前尚不完全清楚您想问什么，以及两种情况下 1 和 2 之间的实际差异是什么，但从基本的数学角度来看:

参数多态函数

f 实际上具有类型 f::forall a.a->int

对于 Haskell 所基于的类型化 lambda 演算中的函数来说，这是一个完全合法的类型。它可以是这样的:

f = λa:Type.λx:a.(body for f)

如何从中获取Double->Int？您将其应用到Double类型:

f Double = (λa:Type.λx:a.(body for f)) Double => λx:Double.(body for f|a=Double)

Haskell 在后台执行这两种操作(类型抽象和类型应用)，尽管可以使用 XExplicitForAll GHC 扩展在类型签名中显式声明 forall 部分，并显式创建一个具有类型签名的 f 的 Double->Int 实例:

f_double :: Double -> Int
f_double = f

高等种类

考虑一个简单的类型:

data Example = IntVal Int | NoVal

(是的，它是Maybe Int)。

Maybe 是一个 type 构造函数，就像 IntVal 是一个 data 构造函数。这是完全相同的事情，只是“高一级”，从某种意义上说，Maybe 应用于 Type，就像应用 IntVal 一样到Int。

在 lambda 演算中，也许 具有类型:

Maybe : Type->Type

Haskell 不允许您从类型构造函数中获取类型，但允许您获取种类(这只是类型的类型的一个奇特名称) :

:k Maybe
Maybe :: * -> *

所以不，Maybe 不是类型:您不能拥有类型为 Maybe 的对象。 Maybe(几乎)是一个从类型到类型的函数，就像 IntVal 是一个从值到值的函数。

我们将 Maybe 应用到 String 的结果称为 Maybe String，就像我们调用应用 IntVal 的结果一样code> 到 4 为 IntVal 4。