Haskell/多态性

类型乐趣

多态性
存在量化的类型
高级类型类
幽灵类型
广义代数数据类型 (GADT)
数据类型代数
 类型构造器和种类

参数多态性

章节目标 = 简短，使读者能够阅读包含 ∀ 的代码 (ParseP) 并使用库 (ST) 而不感到恐惧。这个问题 Talk:Haskell/The_Curry-Howard_isomorphism#Polymorphic types 将由本节解决。

链接到以下论文：Luca Cardelli: On Understanding Types, Data Abstraction, and Polymorphism.

`forall a`

多态函数是适用于多种不同类型的函数。例如，

  length :: [a] -> Int

可以计算任何列表的长度，无论是字符串 String = [Char] 还是整数列表 [Int]。类型变量 a 表示 length 接受任何元素类型。其他多态函数的示例是

  fst :: (a, b) -> a
  snd :: (a, b) -> b
  map :: (a -> b) -> [a] -> [b]

类型变量始终以小写字母开头，而像 Int 或 String 这样的具体类型始终以大写字母开头。这使我们能够区分它们。

有一种更显式的方法来表明 a 可以是任何类型

 length :: forall a. [a] -> Int

换句话说，“对于所有类型 a，函数 length 接受一个类型为 a 的元素列表并返回一个整数”。您应该将旧签名视为带有 forall 关键字的新签名的缩写^[1]。也就是说，编译器会在内部为您插入任何缺失的 forall。另一个例子：fst 的类型签名实际上是

  fst :: forall a. forall b. (a,b) -> a

或等效地

  fst :: forall a b. (a,b) -> a

类似地，map 的类型实际上是

  map :: forall a b. (a -> b) -> [a] -> [b]

这种概念，即某些东西适用于所有类型或对所有事物都成立，被称为全称量化。在数学逻辑中，符号 ∀^[2]（一个倒置的 A，读作“对所有”）通常用于此；它被称为全称量词。

高阶类型

使用显式的 forall，现在可以编写期望多态参数的函数，例如

  foo :: (forall a. a -> a) -> (Char,Bool)
  foo f = (f 'c', f True)

这里，f 是一个多态函数，它可以应用于任何东西。特别是，foo 可以将它应用于字符 'c' 和布尔值 True。

在 Haskell98 中无法编写像 foo 这样的函数，类型检查器会抱怨 f 只能应用于类型为 Char 或类型为 Bool 的值，并拒绝定义。我们最接近 foo 的类型签名的是

  bar :: (a -> a) -> (Char, Bool)

这与

  bar :: forall a. ((a -> a) -> (Char, Bool))

相同。但这与 foo 大不相同。最外层 的 forall 意味着 bar 承诺与任何参数 f 一起使用，只要 f 的形状为 a -> a，对于某个 bar 不知道的类型 a。将此与 foo 相比，在 foo 中，是参数 f 承诺其形状为 a -> a，适用于所有类型 a，并且是 foo 利用了该承诺，通过选择 a = Char 和 a = Bool。

关于命名法，像 bar 这样的简单多态函数被称为具有rank-1 类型，而类型 foo 被归类为rank-2 类型。一般而言，rank-n 类型是至少有一个 rank-(n-1) 参数但没有更高秩参数的函数。

高阶类型的理论基础是System F，也称为二阶 lambda 演算。我们将在System F 部分详细介绍它，以便更好地理解 forall 的含义及其在 foo 和 bar 中的放置。

Haskell98 基于Hindley-Milner 类型系统，它是 System F 的一个受限版本，不支持 forall 和 rank-2 类型或更高秩的类型。您必须启用 RankNTypes^[3] 语言扩展才能利用 System F 的全部功能。

Haskell98 不支持高阶类型是有充分理由的：类型推断 对于完整的 System F 是不可判定的；程序员必须写下所有类型签名。因此，早期版本的 Haskell 采用了 Hindley-Milner 类型系统，它只提供简单的多态函数，但作为交换，它能够实现完整的类型推断。最近的研究进展减少了编写类型签名的负担，并在当前的 Haskell 编译器中使 rank-n 类型变得实用。

`runST`

对于实际的 Haskell 程序员来说，ST 单子可能是现实中 rank-2 类型的第一个例子。类似于 IO 单子，它提供了可变引用

  newSTRef   :: a -> ST s (STRef s a)
  readSTRef  :: STRef s a -> ST s a
  writeSTRef :: STRef s a -> a -> ST s ()

和可变数组。类型变量 s 表示正在操作的状态。但与 IO 不同，这些有状态的计算可以在纯代码中使用。特别是，函数

  runST :: (forall s. ST s a) -> a

设置初始状态，运行计算，丢弃状态并返回结果。如您所见，它具有 rank-2 类型。为什么呢？

重点是可变引用应该在单个 runST 中是局部的。例如，

  v   = runST (newSTRef "abc")
  foo = runST (readSTRef v)

是错误的，因为在一个 runST 的上下文中创建的可变引用在第二个 runST 中再次使用。换句话说，(forall s. ST s a) -> a 中的结果类型 a 可能不是像 v 情况下的 STRef s String 这样的引用。但 rank-2 类型恰好保证了这一点！因为参数必须在 s 中是多态的，所以它必须对所有状态 s 返回相同类型 a；结果 a 不会依赖于状态。因此，上面的错误代码段包含类型错误，编译器会拒绝它。

您可以在原始论文 Lazy functional state threads^[4] 中找到对 ST 单子的更详细解释。

非预言性

predicative = 类型变量被实例化为monotypes。impredicative = 也称为polytypes。例如：length [id :: forall a . a -> a] 或 Just (id :: forall a. a -> a)。与高阶类型略有不同。

通过其通用性来关联多态类型，即 isInstanceOf。
haskell-cafe：RankNTypes 简要说明。

有界参数多态性

类型类

待办事项

System F

本节目标 = 一点 Lambda 演算基础，防止由于隐式类型参数传递而导致的脑损伤。

System F = 所有 ∀-stuff 的基础。
显式类型应用，例如 map Int (+1) [1,2,3]。∀ 类似于函数箭头 ->。
项依赖于类型。大 Λ 用于类型参数，小 λ 用于值参数。

示例

本节目标 = 使读者能够判断是否在自己的代码中使用带有 ∀ 的数据结构。

Church 数，任意递归类型的编码（正性条件）：&forall x. (F x -> x) -> x
Continuation，模式匹配：maybe，either 和 foldr

即 ∀ 可以很好地用于在 Haskell 中实现数据类型。

其他形式的多态性

到目前为止，我们主要讨论了参数多态性。然而，还有两种多态性形式主要用于其他编程语言。

特设多态性
子类型多态性

特设多态性

在 C++ 中，特设多态性可以看作等同于函数重载。

int square(int x);
float square(float x);

我们可以在 Haskell 中使用类型类做类似的事情。

class Square a where
    square :: a -> a
    
instance Square Int where
    square x = x * x

instance Square Float where
    square x = x * x

特设多态性的主要要点是，总会存在函数无法接受的类型，虽然函数可以接受的类型数量可能是无限的。将其与参数多态性进行对比，参数多态性在 C++ 中等同于模板函数。

template <class T>
T id(T a) {
    return a;
}

template <class A, class B>
A const_(A first, B second) {
    return first;
}

template <class T>
int return10 (T a) {
    return 10;
}

这等同于 Haskell 中的以下内容。

id :: a -> a
id a = a

const :: a -> b -> a
const a _ = a

return10 :: a -> Int
return10 _ = 10

参数多态性的主要要点是，任何类型都必须作为函数的输入被接受，无论其返回类型是什么。

请注意，对于这两种多态性形式，都不可能拥有两个仅在返回类型上不同的同名函数。

例如，以下 C++ 代码无效

void square(int x);
int square(int x);

以及 Haskell 版本。

class Square a where
    square :: a -> a
    
instance Square Int where
    square x = x*x

instance Square Int where
    square x = ()

因为编译器无法确定在给定任意函数调用时使用哪个版本。

子类型多态性

待办事项 = 对比 OOP 中的多态性及其相关内容。

自由定理

本节目标 = 使读者能够提出自由定理。无需证明，直觉就足够了。

参数多态性的自由定理。

备注

↑ 请注意，关键字 forall 不是 Haskell 98 标准的一部分，但任何语言扩展 ScopedTypeVariables、Rank2Types 或 RankNTypes 都将在编译器中启用它。未来的 Haskell 标准将包含其中之一。
↑ UnicodeSyntax 扩展允许您在 Haskell 源代码中使用符号 ∀ 代替 forall 关键字。
↑ 或者，如果您只想使用 rank-2 类型，则只需启用 Rank2Types。
↑ John Launchbury (1994-??-??). "Lazy functional state threads". ACM Press": 24–35. {{cite journal}}: Cite journal requires |journal= (help); Check date values in: |date= (help); Unknown parameter |coauthor= ignored (|author= suggested) (help)