Haskell存现句类型辨析

Question

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

我的疑虑

• 在上面PDF的第20页中，下面的代码提到，函数不可能需要特定的缓冲区。为什么会这样？当我起草一个函数时，我完全知道我要使用什么样的缓冲区，尽管我可能不知道我要将什么数据放入其中。使用::Worker MemoryBuffer int有什么不对的，如果他们真的想要抽象缓冲区，他们可以使用一个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

null

Answer 1

GADT通过提供隐式ForAll为使用存在类型的代码提供了清晰、更好的语法

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

data SomeType = forall a. SomeType a

或带有约束：

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

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

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

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

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

我想这并不遥远，尽管您不必使用typeable或data来使用存在类型。我认为更准确的说法是，存在类型提供了一个围绕未指定类型的类型良好的“框”。框确实在某种意义上“隐藏”了类型，这允许您制作这类框的异构列表，忽略它们包含的类型。结果是，像上面的sometype'这样的不受约束的存在式是非常没用的，而是一个受约束的类型：

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

允许您使用模式匹配来窥视“框”内部，并使type类工具可用：

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

注意，这适用于任何类型类，而不仅仅是typeable或data。

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

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

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

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 }

而对存在的worker'值进行操作的类似doWork的函数实现为：

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

对于只有一个函数的type类，字典实际上优化为newtype，因此在本例中，存在的worker类型包括一个隐藏字段，该字段由指向缓冲区的output函数的函数指针组成，这是DoWork所需的唯一运行时信息。