haskell - "exists"在 Haskell 类型系统中意味着什么？

Question

我正在努力理解 exists与 Haskell 类型系统相关的关键字。据我所知，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 类型类中给出的钩子(Hook)。

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 类型类指定的接口(interface)的播放器。

考虑构造函数 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