Haskell/多态性

参数多态性

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

链接到以下论文：Luca Cardelli：理解类型、数据抽象和多态性。

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 关键字的新签名的缩写。也就是说，编译器将在内部为您插入任何缺少的 forall。另一个例子：fst 的类型签名实际上是 forall a b. (a, b) -> a 的简写

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

或等效地

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

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

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

这个概念，即某事物适用于所有类型或对所有事物都成立，被称为全称量化。在数学逻辑中，符号 ∀（一个倒置的 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 这样的简单多态函数被称为具有秩 1 类型，而类型 foo 被归类为秩 2 类型。一般来说，秩 n 类型是一个函数，它至少有一个秩 (n-1) 参数，但没有任何更高秩的参数。

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

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

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

runST

对于实际的 Haskell 程序员来说，ST 单子 可能是野生状态下秩 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

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

关键在于可变引用应该局限在一个 `runST` 中。例如：

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

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

您可以在原始论文 Lazy functional state threads 中找到有关 ST 单子的更详细解释。

非谓词性

• 谓词性 = 类型变量实例化为单类型。非谓词性 = 也是多类型。例如：`length [id :: forall a . a -> a]` 或 `Just (id :: forall a. a -> a)`。与高阶类型略有不同。

• 多态类型根据其通用性（即 `isInstanceOf`）的关系。
• haskell-cafe：RankNTypes 简短解释。

有界参数多态性

类型类

待办事项

系统 F

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

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

例子

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

• Church 数，任意递归类型的编码（正性条件）：`forall x. (F x -> x) -> x`
• 延续，模式匹配：`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 中的多态性和相关内容。

自由定理

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

• 参数多态性的自由定理。

另请参阅

• Luca Cardelli. On Understanding Types, Data Abstraction, and Polymorphism.