ExistentialQuantification

这是一种类型系统扩展,它允许存在量化的类型,换句话说,具有仅在运行时实例化的类型变量

存在类型的值类似于面向对象语言的抽象基类的引用:你不知道确切的类型包含,但可以约束的的类型。

data S = forall a. Show a => S a

或等效地,使用 GADT 语法:

{-# LANGUAGE GADTs #-}
data S where
   S::Show a => a -> S

存在类型为几乎异质的容器打开了大门:如上所述,S 值实际上可以有各种类型,但它们都可以是 shown,因此你也可以做

instance Show S where
    show (S a) = show a   -- we rely on (Show a) from the above

现在我们可以创建这样的对象的集合:

ss = [S 5, S "test", S 3.0]

这也允许我们使用多态行为:

mapM_ print ss

存在感可能非常强大,但请注意,在 Haskell 中它们实际上并不常见。在上面的例子中,你实际上可以用 Show 实例做的就是显示(duh!)值,即创建一个字符串表示。因此,整个 S 类型包含与显示时所获得的字符串完全相同的信息。因此,通常最好简单地立即存储该字符串,特别是因为 Haskell 是懒惰的,因此字符串最初只是一个未评估的 thunk。

另一方面,存在会导致一些独特的问题。例如,类型信息在存在主义中隐藏的方式。如果你对 S 值进行模式匹配,你将在范围内包含所包含的类型(更准确地说,它的 Show 实例),但是这个信息永远不会转义它的范围,因此它变成了一个秘密社会:编译器除了从外部已知类型的值之外,不会让任何东西转义范围。这可能导致Couldn't match type ‘a0’ with ‘()’ ‘a0’ is untouchable 这样的奇怪错误。

将此与普通参数多态进行对比,这通常在编译时解决(允许完全类型擦除)。

存在类型与 Rank-N 类型不同 - 粗略地说,这些扩展是彼此双重的:要实际使用存在类型的值,你需要一个(可能是约束的)多态函数,如示例中的 show。多态函数是普遍量化的,即它适用于给定类中的任何类型,而存在量化意味着它适用于某种特定类型,这是先验未知的。如果你有一个多态函数,那就足以传递多态函数,比如参数,你需要 {-# LANGUAGE Rank2Types #-}

genShowSs :: (∀ x . Show x => x -> String) -> [S] -> [String]
genShowSs f = map (\(S a) -> f a)