Haskell/存在量化的类型

存在量化的类型 (解决方案)

类型乐趣

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

存在类型，或者简称为“存在”，是一种将一组类型“压缩”成一个单一类型的类型。

存在是 GHC 的类型系统扩展的一部分。它们不是 Haskell98 的一部分，因此您必须使用额外的命令行参数 -XExistentialQuantification 编译包含它们的任何代码，或者在使用存在的源代码顶部添加 {-# LANGUAGE ExistentialQuantification #-} 。

`forall` 关键字

forall 关键字用于显式地将新的类型变量引入作用域。例如，考虑一下您已经无意中写过一百次的东西

示例： 多态函数

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

但这些 a 和 b 是什么呢？嗯，它们是类型变量，你回答说。编译器看到它们以小写字母开头，因此允许任何类型来填充该角色。另一种说法是这些变量是“普遍量化的”。如果您学习过形式逻辑，您一定遇到过量词：“对所有”（或 $\forall$ ）和“存在”（或 $\exists$ ）。它们对后面的内容进行“量化”：例如， $\exists x$ 表示后面的内容对至少一个 x 值成立。 $\forall x$ 表示后面的内容对您可以想象的任何可能的 x 值都成立。例如， $\forall x,\,x^{2}\geq 0$ 和 $\exists x,\,x^{3}=27$ 。

forall 关键字以类似的方式对类型进行量化。我们将 map 的类型改写如下

示例： 显式地量化类型变量

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

所以我们看到，对于我们可以想象的任何 a 和 b 类型组合，map 都采用 (a -> b) -> [a] -> [b] 类型。例如，我们可能选择 a = Int 和 b = String。那么说 map 的类型是 (Int -> String) -> [Int] -> [String] 是有效的。在这里，我们将 map 的通用类型实例化为更具体的类型。

但是，在 Haskell 中，任何小写类型参数的引入都隐含地以 forall 关键字开头，因此前面两个关于 map 的类型声明是等价的，下面的声明也是如此

示例： 两个等效的类型语句

id :: a -> a
id :: forall a . a -> a

真正有趣的是，forall 的作用是你可以对它引入的类型变量施加额外的约束。这些约束， $P(x)$ ，充当对类型变量， $x$ ，的某种保证特定属性的限制，（类似于 $\exists x,P(x)$ 或 $\forall x,P(x)$ 规定）。

让我们直接深入了解，看看存在类型在实际中的强大功能。

示例：异构列表

Haskell 类型类系统的基本前提是将所有共享相同属性的类型分组。因此，如果您知道一个类型是某个类 C 的成员，那么您就知道该类型的某些信息。例如，Int 是类 Eq 的成员，所以我们知道 Int 的元素可以比较相等。

假设我们有一组值。我们不知道它们是否都属于相同的类型，但我们知道它们都是某个类的成员（并且，通过扩展，所有值都具有一定的属性）。将所有这些值放入一个列表中可能很有用。我们通常无法做到这一点，因为列表元素必须具有相同的类型（类型方面是同构的）。但是，存在类型允许我们通过定义“类型隐藏器”或“类型框”来放松此要求。

示例：构建异构列表

 data ShowBox = forall s. Show s => SB s
 
 heteroList :: [ShowBox]
 heteroList = [SB (), SB 5, SB True]

我们不会详细解释数据类型定义的含义，但其含义应该很直观。重要的是，我们正在对三种不同类型的三个值调用构造函数，[SB (), SB 5, SB True]，但我们能够将它们全部放入一个列表中，因此我们必须以某种方式为每个值拥有相同的类型。本质上，是的。这是因为我们对 forall 关键字的使用为我们的构造函数提供了类型 SB :: forall s. Show s => s -> ShowBox。如果我们现在要编写一个打算将 heteroList 传递给它的函数，我们不能对 SB 中的值应用像 not 这样的函数，因为它们的类型可能不是 Bool。但我们确实知道每个元素的一些信息：它们可以通过 show 转换为字符串。实际上，这几乎是我们知道的关于它们唯一的知识。

示例：使用我们的异构列表

 instance Show ShowBox where
  show (SB s) = show s        -- (*) see the comment in the text below
 
 f :: [ShowBox] -> IO ()
 f xs = mapM_ print xs

 main = f heteroList

让我们更详细地说明一下。在 ShowBox 的 show 定义中 - 标记为 (*) 请参阅下面的文本中的注释 的行 - 我们不知道 s 的类型。但正如我们提到的，我们确实知道该类型是 Show 的实例，因为 SB 构造函数上的约束。因此，对 s 使用函数 show 是合法的，如函数定义的右侧所示。

至于 f，请回忆 print 的类型

示例：相关函数的类型

 print :: Show s => s -> IO () -- print x = putStrLn (show x)
 mapM_ :: (a -> m b) -> [a] -> m ()
 mapM_ print :: Show s => [s] -> IO ()

正如我们刚刚声明 ShowBox 是 Show 的实例，我们可以打印列表中的值。

进一步解释

理解 forall 的一种方法是将类型视为一组可能的值。例如，Bool 是集合 {True, False, ⊥}（记住，底部，⊥，是每种类型的成员！），Integer 是整数的集合（以及底部），String 是所有可能的字符串的集合（以及底部），等等。forall 充当断言指定类型（即值的集合）之间共性或交集的一种方式。例如，forall a. a 是所有类型的交集。这个子集恰好是只有底部元素 {⊥} 的集合，因为它是在每种类型中的一个隐式值。也就是说，只有底部的值可用的类型。但是，由于每个 Haskell 类型都包含底部，{⊥}，因此这种量化实际上规定了所有 Haskell 类型。但是，允许对它的唯一操作是那些可用于其唯一元素是底部的类型的操作。

更多示例

列表 [forall a. a] 是元素类型均为 forall a. a 的列表的类型，即底部列表。
列表 [forall a. Show a => a] 是元素类型均为 forall a. Show a => a 的列表的类型。Show 类约束要求可能的类型也是类 Show 的成员。但是，⊥ 仍然是所有这些类型的唯一公共值，因此这也是一个底部列表。
列表 [forall a. Num a => a] 要求每个元素都是类 Num 的成员。因此，可能的值包括数字文字，其具有特定类型 forall a. Num a => a，以及底部。
forall a. [a] 是元素类型均为 a 的列表的类型。由于我们根本无法假定任何特定类型，因此这也是一个底部列表。

我们看到，大多数类型上的交集只会导致底部，因为类型通常没有任何共同的值，因此无法对它们的联合值做出假设。

但是，请记住，在上节中，我们使用“类型隐藏器”开发了一个异构列表。这个“类型隐藏器”充当包装类型，通过暗示对允许类型施加的谓词或约束来保证某些功能。在这种情况下，它们必须是类型类 Show 的成员。一般来说，这似乎是 forall 的目的，即对类型声明中允许的类型施加类型约束，从而保证使用此类类型的某些功能。

让我们声明一个。

示例：存在类型

 data T = forall a. MkT a

这意味着

示例：这定义了一个多态构造函数，或一个用于 T 的构造函数系列。

MkT :: forall a. (a -> T)

因此，我们可以将任何我们想要传递给 MkT 的类型 a 传递给它，它将创建一个 T。那么，当我们使用模式匹配来解构 T 值时会发生什么？…

示例：对我们的存在构造函数进行模式匹配

 foo (MkT x) = ... -- what is the type of x?

正如我们刚刚提到的，x 可以是任何类型。这意味着它是一些任意类型的成员，因此具有类型 forall a. a。换句话说，只有底部 ⊥ 可用的集合。

但是，我们可以创建一个异构列表

示例：构建异构列表

 heteroList = [MkT 5, MkT (), MkT True, MkT map]

当然，当我们对 heteroList 进行模式匹配时，我们不能对它的元素做出任何假设^[1]。因此，从技术上讲，除了将它们简化为 WHNF^[2] 之外，我们不能对它的元素做任何有用的操作。但是，如果我们引入类约束

示例：一个新的存在数据类型，带有类约束

 data T' = forall a. Show a => MkT' a

类约束用于限制我们正在交叉的类型，这样我们现在在 T' 中的值是属于 Show 的成员 的某些任意类型的元素。这意味着我们可以将 show 应用于解构后类型为 a 的值。无论该值实际是什么类型都无关紧要。

示例：使用我们新的异构设置

 heteroList' = [MkT' 5, MkT' (), MkT' True, MkT' "Sartre"]
 main = mapM_ (\(MkT' x) -> print x) heteroList'

 {- prints:
 5
 ()
 True
 "Sartre"
 -}

总之，通用量词与数据类型的交互产生了一个限定的类型子集，保证了由一个或多个类约束描述的某些功能。

示例：`runST`

您可能尚未遇到的一种单子是 ST 单子。这本质上是 State 单子的一个更强大的版本：它具有更复杂的结构，并且涉及一些更高级的主题。它最初是为了为 Haskell 提供 IO 而编写的。正如我们在Understanding monads 章节中提到的，IO 本质上只是具有包含有关现实世界的所有信息的“环境”的 State 单子。实际上，至少在 GHC 内部，使用 ST，并且环境是一种称为 RealWorld 的类型。

要退出 State 单子，您可以使用 runState。ST 的类似函数称为 runST，它具有一种非常特殊的类型

示例：runST 函数

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

这实际上是更复杂语言特征（称为 rank-2 多态性）的示例，我们在此不做详细介绍。重要的是要注意，没有用于初始状态的参数。实际上，ST 使用与 State 不同的状态概念；虽然 State 允许您 get 和 put 当前状态，但 ST 提供了对引用的接口。您可以使用 newSTRef :: a -> ST s (STRef s a) 创建引用（类型为 STRef），提供初始值，然后您可以使用 readSTRef :: STRef s a -> ST s a 和 writeSTRef :: STRef s a -> a -> ST s () 来操作它们。因此，ST 计算的内部环境不是一个特定值，而是一个从引用到值的映射。因此，您不需要为 runST 提供初始状态，因为初始状态只是不包含任何引用的空映射。

但是，事情并不像看起来那样简单。是什么阻止您在一个 ST 计算中创建引用，然后在另一个计算中使用它？我们不想允许这样做，因为（出于线程安全的原因）不应该允许任何 ST 计算假设初始内部环境包含任何特定引用。更具体地说，我们希望以下代码无效

示例：错误的 ST 代码

 let v = runST (newSTRef True)
 in runST (readSTRef v)

是什么能阻止这种情况？runST 类型中 rank-2 多态性的效果是限制类型变量 s 的范围 在第一个参数内。换句话说，如果类型变量 s 出现在第一个参数中，它就不能出现在第二个参数中。让我们看一下这到底是如何完成的。假设我们有一些类似以下代码的代码

示例：更简洁的错误 ST 代码

... runST (newSTRef True) ...

编译器尝试将类型组合在一起

示例：编译器的类型检查阶段

newSTRef True :: forall s. ST s (STRef s Bool)
runST :: forall a. (forall s. ST s a) -> a
together, (forall s. ST s (STRef s Bool)) -> STRef s Bool

第一个方括号中 forall 的重要性在于我们可以更改 s 的名称。也就是说，我们可以写

示例：类型不匹配！

together, (forall s'. ST s' (STRef s' Bool)) -> STRef s Bool

这很有道理：在数学中，说 $\forall x.x>5$ 与说 $\forall y.y>5$ 完全相同；你只是给变量起了不同的标签。然而，我们上面的代码存在一个问题。请注意，因为 forall 不作用于 runST 的返回值类型，我们也没有将那里的 s 重命名。但突然之间，我们出现了类型不匹配！第一个参数中 ST 计算的结果类型必须与 runST 的结果类型匹配，但现在它们不匹配了！

存在量词的关键特征在于，它允许编译器泛化第一个参数中状态的类型，因此结果类型不能依赖于它。这巧妙地绕开了我们的依赖性问题，并将对 runST 的每次调用“隔离”到它自己的小堆中，引用无法在不同的调用之间共享。

量化类型作为积和和

一个全称量化类型可以被解释为类型的无限积。例如，像

示例： 恒等函数

 id :: forall a. a -> a
 id a = a

这样的多态函数可以理解为一个积，或者一个元组，其中包含每个可能的类型 a 的单个函数。要构造这种类型的的值，我们必须一次性提供元组的所有组成部分。对于函数类型来说，由于多态性，这是可能的——一个公式生成无限多个函数。

对于数值类型，可以使用一个数值常量来一次性初始化多个类型。例如，在

示例： 多态值

 x :: forall a. Num a => a
 x = 0

中，x 可以被理解为一个元组，它包含一个 Int 值、一个 Double 值等等。

类似地，一个存在量化类型可以被解释为一个无限和。例如，

示例： 存在类型

 data ShowBox = forall s. Show s => SB s

可以被理解为一个和

示例： 和类型

 data ShowBox = SBUnit | SBInt Int | SBBool Bool | SBIntList [Int] | ...

要构造这种类型的的值，我们只需要选择一个构造函数。一个多态构造函数 SB 将所有这些构造函数组合成一个。

量化作为一种基元

全称量化对于定义尚未定义的数据类型很有用。假设 Haskell 中没有内置的配对。可以使用量化来定义它们。

{-# LANGUAGE ExistentialQuantification, RankNTypes #-}

newtype Pair a b = Pair (forall c. (a -> b -> c) -> c)

makePair :: a -> b -> Pair a b
makePair a b = Pair $ \f -> f a b

在 GHCi 中

 λ> :set -XExistentialQuantification
 λ> :set -XRankNTypes
 λ> newtype Pair a b = Pair {runPair :: forall c. (a -> b -> c) -> c}
 λ> makePair a b = Pair $ \f -> f a b
 λ> pair = makePair "a" 'b' 
 
 λ> :t pair
 pair :: Pair [Char] Char
 
 λ> runPair pair (\x y -> x)
 "a"
 
 λ> runPair pair (\x y -> y)
 'b'