haskell - 澄清 Haskell 中的存在类型

Question

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

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

存在类型似乎对它们包含的类型不感兴趣，但与它们匹配的模式表明存在某种类型，除非我们使用 Typeable 或 Data，否则我们不知道它是什么类型。

当我们想要隐藏类型时(例如:用于异构列表)或者我们在编译时并不真正知道类型是什么时，我们会使用它们。

GADT '通过提供隐式 forall 为使用存在类型的代码提供清晰和更好的语法的

我的疑惑

在上述 PDF 的第 20 页中，以下代码提到函数不可能要求特定的缓冲区。为什么会这样？当我起草一个函数时，我确切地知道我要使用什么样的缓冲区，尽管我可能不知道我要放入什么数据。
有什么问题 :: 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 表，然后在运行时它会从 V 表中计算出来？如果是这样，那么它将存储什么样的信息？

Answer 1

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

我认为普遍认为 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 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使用存在类型。我认为说存在类型在未指定类型周围提供了一个类型良好的“盒子”会更准确。从某种意义上说，盒子确实“隐藏”了类型，这使您可以制作此类盒子的异构列表，而忽略它们包含的类型。事实证明，一个不受约束的存在，如 SomeType'上面是非常没用的，但是一个受约束的类型:

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

允许您进行模式匹配以窥视“盒子”内部并使类型类设施可用:

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

请注意，这适用于任何类型类，而不仅仅是 Typeable或 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

但是如果你编写一个函数，它需要一个 Worker作为参数，它只能使用一般 Buffer类型类设施(例如，函数 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 type 包括一个隐藏字段，该字段由指向 output 的函数指针组成。缓冲区的函数，这是 doWork 所需的唯一运行时信息.