Haskell 中存在类型的说明

Question

我试图理解 Haskell 中的存在类型并遇到了一个 PDF http://www.ii.uni.wroc.pl/~dabi/courses/ZPF15/rlasocha/prezentacja.pdf

请纠正我目前的以下理解。

存在类型似乎对它们包含的类型不感兴趣，但模式匹配它们说存在某种类型我们不知道它是什么类型，除非我们使用 Typeable 或 Data。
当我们想要隐藏类型（例如：对于异构列表）或者我们真的不知道编译时的类型时，我们会使用它们。
GADT 通过提供隐式 forall

我的疑惑

在上面PDF的第20页中，下面的代码提到了一个Function不可能要求特定的Buffer。为什么会这样？当我起草一个函数时，我确切地知道我要使用什么样的缓冲区，尽管我可能不知道我要将什么数据放入其中。 Having :: Worker MemoryBuffer Int 有什么问题如果他们真的想通过 Buffer 进行抽象，他们可以有一个 Sum 类型 data Buffer = MemoryBuffer | NetBuffer | RandomBuffer 并且有一个像 :: Worker Buffer Int

data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

因为 Haskell 是像 C 一样的全类型擦除语言，那么它如何在运行时知道要调用哪个函数。是不是有点像我们要维护一些信息并传入一个巨大的函数 V-Table，然后在运行时它会从 V-Table 中计算出来？如果是这样，那么它将存储什么样的信息？

Answer 1

GADT's provide the clear & better syntax to code using Existential Types by providing implicit forall's

我认为普遍认为 GADT 语法更好。我不会说这是因为 GADT 提供隐式 forall，而是因为使用 ExistentialQuantification 扩展启用的原始语法可能是 confusing/misleading。当然，该语法看起来像：

data SomeType = forall a. SomeType a

或有约束条件：

data SomeShowableType = forall a. Show a => SomeShowableType a

而且我认为共识是这里使用关键字 forall 使得类型很容易与完全不同的类型混淆：

data AnyType = AnyType (forall a. a)    -- need RankNTypes extension

更好的语法可能使用单独的 exists 关键字，因此您应该写：

data SomeType = SomeType (exists a. a)   -- not valid GHC syntax

GADT 语法，无论是隐式还是显式 forall，在这些类型中都更加统一，而且似乎更容易理解。即使使用显式 forall，以下定义也传达了这样的想法，即您可以采用任何类型的值 a 并将其放入单态 SomeType':

data SomeType' where
    SomeType' :: forall a. (a -> SomeType')   -- parentheses optional

并且很容易看出和理解该类型与：

之间的区别

data AnyType' where
    AnyType' :: (forall a. a) -> AnyType'

Existential Types not seem to be interested in the type they contain but pattern matching them say that there exists some type we don't know what type it is until & unless we use Typeable or Data.

We use them when we want to Hide types (ex: for Heterogeneous Lists) or we don't really know what the types at Compile Time.

我想这些并不太远，尽管您不必使用 Typeable 或 Data 来使用存在类型。我认为说存在类型围绕未指定类型提供类型良好的 "box" 会更准确。该框在某种意义上 "hide" 类型，这使您可以创建此类框的异构列表，而忽略它们包含的类型。事实证明，像上面的 SomeType' 这样的不受约束的存在是非常无用的，但是受约束的类型：

data SomeShowableType' where
    SomeShowableType' :: forall a. (Show a) => a -> SomeShowableType'

允许您进行模式匹配以查看 "box" 内部并使类型 class 设施可用：

showIt :: SomeShowableType' -> String
showIt (SomeShowableType' x) = show x

请注意，这适用于任何类型 class，而不仅仅是 Typeable 或 Data。

关于您对幻灯片第 20 页的困惑，作者说函数 需要一个存在 Worker 来要求一个Worker 有一个特定的 Buffer 实例。您可以编写一个函数来使用特定类型的 Buffer 创建 Worker，例如 MemoryBuffer:

class Buffer b where
  output :: String -> b -> IO ()
data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer
instance Buffer MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

但是如果你写一个函数接受一个 Worker 作为参数，它只能使用一般的 Buffer 类型 class 设施（例如函数 output ):

doWork :: Worker Int -> IO ()
doWork (Worker b x) = output (show x) b

它不能试图要求 b 成为特定类型的缓冲区，即使通过模式匹配也是如此：

doWorkBroken :: Worker Int -> IO ()
doWorkBroken (Worker b x) = case b of
  MemoryBuffer -> error "try this"       -- type error
  _            -> error "try that"

最后，有关存在类型的运行时信息可通过所涉及类型class 的隐式 "dictionary" 参数获得。上面的 Worker 类型，除了有用于缓冲区和输入的字段外，还有一个不可见的隐式字段，它指向 Buffer 字典（有点像 v-table，虽然它几乎没有很大，因为它只包含一个指向适当 output 函数的指针。

在内部，类型 class Buffer 表示为具有函数字段的数据类型，实例是 "dictionaries" 这种类型：

data Buffer' b = Buffer' { output' :: String -> b -> IO () }

dBuffer_MemoryBuffer :: Buffer' MemoryBuffer
dBuffer_MemoryBuffer = Buffer' { output' = undefined }

存在类型对此字典有一个隐藏字段：

data Worker' x = forall b. Worker' { dBuffer :: Buffer' b, buffer' :: b, input' :: x }

并且像 doWork 这样对存在的 Worker' 值进行操作的函数实现为：

doWork' :: Worker' Int -> IO ()
doWork' (Worker' dBuf b x) = output' dBuf (show x) b

对于只有一个函数的类型class，字典实际上被优化为一个新类型，所以在这个例子中，存在的Worker类型包括一个由函数指针组成的隐藏字段到缓冲区的 output 函数，这是 doWork.

唯一需要的运行时信息

Answer 2

In Page 20 of above PDF it is mentioned for below code that it is impossible for a Function to demand specific Buffer. Why is it so?

因为Worker，按照定义，只接受一个参数，即"input"字段的类型（类型变量x）。例如。 Worker Int 是一种类型。相反，类型变量 b 不是 Worker 的参数，而是一种 "local variable"，可以这么说。它不能像 Worker Int String 那样传递——那会触发类型错误。

如果我们改为定义：

data Worker x b = Worker {buffer :: b, input :: x}

然后 Worker Int String 会工作，但类型不再存在 - 我们现在也总是必须传递缓冲区类型。

As Haskell is a Full Type Erasure language like C then How does it know at Runtime which function to call. Is it something like we gonna maintain few information and pass in a Huge V-Table of Functions and at runtime it gonna figure out from V-Table? If it is so then what sort of Information it gonna store?

大致正确。简而言之，每次您应用构造函数 Worker 时，GHC 都会从 Worker 的参数中推断出 b 类型，然后搜索实例 Buffer b。如果找到，GHC 会在对象中包含一个指向该实例的附加指针。在最简单的形式中，这与存在虚函数时添加到 OOP 中每个对象的 "pointer to vtable" 没有太大区别。

不过，在一般情况下，它可能要复杂得多。如果这样可以加快代码速度，编译器可能会使用不同的表示形式并添加更多指针而不是单个指针（例如，直接将指针添加到所有实例方法）。此外，有时编译器需要使用多个实例来满足约束。例如，如果我们需要存储 Eq [Int] 的实例......那么只有两个：一个用于 Int 和一个用于列表，并且需要将两者组合（在运行时间，除非优化）。

很难准确猜测 GHC 在每种情况下的作用：这取决于大量可能会或可能不会触发的优化。

您可以尝试使用 google 搜索类型类的 "dictionary based" 实现，以了解更多关于正在发生的事情。您还可以要求 GHC 使用 -ddump-simpl 打印内部优化的核心，并观察正在构建、存储和传递的字典。我必须警告你：核心是相当低级的，一开始可能很难阅读。

Haskell 中存在类型的说明

Clarification on Existential Types in Haskell

haskell

existential-type

gadt