Haskell类型系统中的"exists"是什么意思？

Question

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

• 有一些扩展可以添加它们，在声明中像这样：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方面并不是完全的新手（也许像二年级学生那样），但我的数学基础还欠缺一些。

- Valentin Golev

---

我期待着一个很棒的答案。谢谢你的提问。 - Alexandre C.

这个链接：http://www.haskell.org/haskellwiki/Existential_type 可能会有所帮助。 - Alexandre C.

“Ctrl-F存在” - 只出现一次，而且不在主文本中...但我正在阅读它，非常感谢。 - Valentin Golev

@valya：是的。那里链接的Essential Haskell博士论文也值得一读。 - Alexandre C.

回答这个问题可能会有所帮助：https://dev59.com/wXA75IYBdhLWcg3w186G - sclv

感谢您的精彩回答。我最喜欢mokus和rampion的回答，但我不知道该选择哪一个。我明天会使用得分最高的答案。 - Valentin Golev

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 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”可以满足特定类型“m”的“Player p m”合同，因此我们给“WpPlayer”构造函数一个特定类型的“p”，以便返回相同的类型。因此，我们不能使用“forall”。我们真正能够说的是存在某些类型“p”，它满足类型“m”的“Player p m”合同。

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

- rampion

---

这是实现面向对象编程的多态性的功能性方法。 - Alexandre C.

Answer 2

当我说forall a. a -> Int时，它的意思是（以我的理解，可能是错误的）“对于每个（类型）a，都存在一个类型为a->Int的函数”：

接近了，但不完全正确。它的意思是“对于每个类型a，可以将此函数视为具有类型a->Int”。因此，a可以专门针对调用者选择的任何类型进行特化。

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

请注意，这意味着这种特定类型（exists a. a -> Int）并不那么有趣-没有有用的方法来调用该函数，除了传递“底部”值，如undefined或let x = x in x。更有用的签名可能是exists a. Foo a => Int -> a。它表示函数返回一个特定类型a，但您不知道它的类型。但是您确实知道它是Foo的一个实例-因此，尽管不知道其“真正”的类型，但可以对其执行一些有用的操作。

- mokus

---

在 Haskell 中不存在 exists 关键字，那么您第二个示例的等价 forall 表示是什么？exists a. Foo a => Int -> a 可以翻译为：对于 Haskell 而言不存在 exists 关键字，因此您的第二个示例中的等价 forall 表示是什么？forall a. Foo a => Int -> a - CMCDragonkai

Answer 3

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

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

正因为如此，以下类型并不是非常有用：

data Useless = exists s. Useless s

因为我无法操作该值（不完全准确；我可以使用seq函数操作），且该值的类型我一无所知。

- Edward Z. Yang

---

也许您可以举一些有用的例子来详细说明一下？非常感谢。（顺便说一句，您的博客很棒，教会了我很多东西） - Valentin Golev

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/

- sclv