Haskell 类型系统中的“存在”是什么意思？

Question

我很难理解与 Haskell 类型系统相关的 exists 关键字。据我所知，Haskell中默认没有这样的关键字，但是：

• 有extensions 将它们添加到类似data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a) 的声明中
• 我看过一篇关于它们的论文，并且（如果我没记错的话）它指出 exists 关键字对于类型系统来说是不必要的，因为它可以被 forall 概括

但我什至无法理解exists 的含义。

当我说 forall a . a -> Int 时，它的意思是（在我的理解中，我猜是不正确的）“对于每个（类型）a，都有一个类型为 a -> Int 的函数”：

myF1 :: forall a . a -> Int
myF1 _ = 123
-- okay, that function (`a -> Int`) does exist for any `a`
-- because we have just defined it

当我说exists a . a -> Int 时，它到底是什么意思？ “至少有一种类型 a 有一个类型为 a -> Int 的函数”？为什么要写这样的声明？目的是什么？语义？编译器行为？

myF2 :: exists a . a -> Int
myF2 _ = 123
-- okay, there is at least one type `a` for which there is such function
-- because, in fact, we have just defined it for any type
-- and there is at least one type...
-- so these two lines are equivalent to the two lines above

请注意，它并不是一个可以编译的真实代码，只是我想象中的一个例子，然后我听说了这些量词。

---

附：我在 Haskell 中并不完全是新手（可能像二年级学生），但我缺乏这些东西的数学基础。

Answer 1

我遇到的存在类型的使用是我的code for mediating a game of Clue。

我的中介代码有点像经销商。它不关心玩家的类型是什么——它只关心所有玩家实现Player 类型类中给出的钩子。

class Player p m where
  -- deal them in to a particular game
  dealIn :: TotalPlayers -> PlayerPosition -> [Card] -> StateT p m ()

  -- let them know what another player does
  notify :: Event -> StateT p m ()

  -- ask them to make a suggestion
  suggest :: StateT p m (Maybe Scenario)

  -- ask them to make an accusation
  accuse :: StateT p m (Maybe Scenario)

  -- ask them to reveal a card to invalidate a suggestion
  reveal :: (PlayerPosition, Scenario) -> StateT p m Card

现在，庄家可以保留Player p m => [p] 类型的玩家列表，但这会限制 所有玩家都属于同一类型。

这太狭窄了。如果我想拥有不同类型的玩家怎么办？ 以不同的方式让它们相互对抗？

所以我使用ExistentialTypes 为玩家创建一个包装器：

-- wrapper for storing a player within a given monad
data WpPlayer m = forall p. Player p m => WpPlayer p

现在我可以轻松地保存一个异类的玩家列表。经销商仍然可以轻松地与 玩家使用Player类型类指定的接口。

考虑构造函数WpPlayer的类型。

    WpPlayer :: forall p. Player p m  => p -> WpPlayer m

除了前面的forall，这是非常标准的haskell。适用于所有类型 满足契约Player p m的p，构造函数WpPlayer映射一个类型为p的值 为 WpPlayer m 类型的值。

有趣的是带有解构函数：

    unWpPlayer (WpPlayer p) = p

unWpPlayer 的类型是什么？这行得通吗？

    unWpPlayer :: forall p. Player p m => WpPlayer m -> p

不，不是真的。一堆不同类型的p 可以满足Player p m 合约 具有特定类型m。我们给WpPlayer 构造函数一个特定的 类型 p，所以它应该返回相同的类型。所以我们不能使用forall。

我们真正能说的是存在某种类型 p，它满足 Player p m 合约 类型为m。

    unWpPlayer :: exists p. Player p m => WpPlayer m -> p

Answer 2

当我说，forall a . a -> 整数，它 意味着（在我的理解中， 不正确的，我猜）“对于每个 （类型）a，有a的功能 键入 a -> Int"：

关闭，但不完全。这意味着“对于每个类型 a，this 函数可以被认为具有类型 a -> Int”。所以a 可以专门用于调用者选择的任何类型。

在“存在”的情况下，我们有：“有一些（特定的，但未知的）类型 a，因此该函数的类型为 a -> Int”。所以a一定是特定类型，但是调用者不知道是什么。

请注意，这意味着这个特定类型 (exists a. a -> Int) 并不是那么有趣 - 除了传递“底部”值（例如 undefined 或 let x = x in x）之外，没有其他有用的方法可以调用该函数。更有用的签名可能是exists a. Foo a => Int -> a。它说函数返回一个特定类型a，但你不知道是什么类型。但是您确实知道它是 Foo 的一个实例 - 因此您可以使用它做一些有用的事情，尽管您不知道它的“真实”类型。

Answer 3

这恰恰意味着“存在一个类型a，我可以在我的构造函数中为其提供以下类型的值。”请注意，这与说“a 的值在我的构造函数中是 Int”不同；在后一种情况下，我知道类型是什么，并且我可以使用我自己的函数，该函数将Ints 作为参数来对数据类型中的值执行其他操作。

因此，从实用的角度来看，存在类型允许您将底层类型隐藏在数据结构中，从而迫使程序员仅使用您在其上定义的操作。它代表封装。

正因为如此，下面的类型不是很有用：

data Useless = exists s. Useless s

因为我对价值无能为力（不完全正确；我可以seq 它）；我对它的类型一无所知。

Answer 4

UHC 实现了 exists 关键字。这是其文档中的一个示例

x2 :: exists a . (a, a -> Int)
x2 = (3 :: Int, id)

xapp :: (exists b . (b,b -> a)) -> a
xapp (v,f) = f v

x2app = xapp x2

还有一个：

mkx :: Bool -> exists a . (a, a -> Int)
mkx b = if b then x2 else ('a',ord)

y1 = mkx True -- y1 :: (C_3_225_0_0,C_3_225_0_0 -> Int)
y2 = mkx False -- y2 :: (C_3_245_0_0,C_3_245_0_0 -> Int)

mixy = let (v1,f1) = y1
            (v2,f2) = y2
       in f1 v2

"mixy 会导致类型错误。但是，我们可以很好地使用 y1 和 y2："

main :: IO ()
main = do putStrLn (show (xapp y1))
          putStrLn (show (xapp y2))

ezyang 也写了很好的博客：http://blog.ezyang.com/2010/10/existential-type-curry/