“存在”是什么？在 Haskell 类型系统中意味着什么？

Question

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

• 有 扩展，在像这样的声明中添加它们：data Accum a = contains s。 MkAccum s (a -> s -> s) (s -> a)
• 我看过一篇关于它们的论文，并且（如果我没记错的话）它指出存在 关键字对于类型系统来说是不必要的，因为它可以通过 forall 进行泛化，

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

当我说，forall 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

当我说存在一个 .一个-> 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

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

---

PS 我不完全是 Haskell 的新手（也许像二年级学生），但我缺乏这些东西的数学基础。

Answer 1

我遇到的存在类型的使用是我的用于调解 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 pm => 类型的玩家列表。 [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。适用于所有类型
p 满足契约 Player p m，构造函数 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

当我说，对于所有 a .一个->内特，它
意味着（在我的理解中，
我猜是错误的）“对于每一个
（类型）a，有a的函数
输入 a ->国际”：

接近，但不完全。它的意思是“对于每个类型a，这个函数可以被认为具有类型a -> Int”。因此 a 可以专门化为调用者选择的任何类型。

在“exists”情况下，我们有：“存在某种（特定但未知）类型 a，使得该函数具有类型a-> Int”。所以a一定是一个特定类型，但调用者不知道是什么。

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

Answer 3

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

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

正是由于这个原因，以下类型不是很有用：

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/