澄清 Haskell 中的存在类型

Question

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

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

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

我的疑惑

• 在上面 PDF 的第 20 页中，下面的代码提到函数不可能要求特定的缓冲区。为什么会这样？当我起草一个函数时，我确切地知道我将使用什么样的缓冲区，尽管我可能不知道我将放入哪些数据。什么是错在有:: Worker MemoryBuffer Int如果他们真的想在抽象缓冲区他们能有一个求和型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 表，然后在运行时它会从 V 表中找出来？如果是这样，那么它将存储什么样的信息？

Answer 1

GADT 通过提供隐式 forall 为使用 Existential Types 的代码提供清晰和更好的语法

我认为大家普遍认为 GADT 语法更好。我不会说这是因为 GADT 提供了隐式 foralls，而是因为使用ExistentialQuantification扩展启用的原始语法可能会造成混淆/误导。当然，这种语法看起来像：

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 似乎对它们包含的类型不感兴趣，但是模式匹配它们说存在某种类型，我们不知道它是什么类型，除非我们使用 Typeable 或 Data。

当我们想要隐藏类型（例如：用于异构列表）或者我们在编译时不知道类型是什么时，我们会使用它们。

我想这些不会太远，尽管您不必使用Typeable或Data使用存在类型。我认为更准确地说，存在类型在未指定的类型周围提供了一个类型良好的“框”。盒子在某种意义上确实“隐藏”了类型，这允许您制作此类盒子的异类列表，而忽略它们包含的类型。事实证明，像SomeType'上面这样的不受约束的存在是非常无用的，但是受约束的类型：

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

允许您进行模式匹配以查看“盒子”内部并使类型类工具可用：

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

请注意，这适用于任何类型的类，而不仅仅是Typeableor Data。

关于你对幻灯片第 20 页的困惑，作者说，一个需要存在 的函数不可能Worker要求Worker有一个特定的Buffer实例。您可以编写一个函数来Worker使用特定类型的来创建Buffer，例如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

但是如果你编写一个以 aWorker作为参数的函数，它只能使用通用Buffer类型类工具（例如， function 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"

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

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

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

对于只有一个函数的类型类，字典实际上被优化为一个新Worker类型，所以在这个例子中，存在类型包括一个隐藏字段，它包含一个指向output缓冲区函数的函数指针，这是唯一需要的运行时信息由doWork.