34

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

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

但我什至无法理解是什么exists意思。

当我说 时forall a . a -> Int，它意味着（在我的理解中，我猜是不正确的）“对于每个 (type) 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

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

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

4

4 回答 4

26

我遇到的存在类型的使用是使用我的代码来调解 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，构造函数将 type 的值WpPlayer映射到 typep 的值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与 type 的约定m。

    unWpPlayer :: exists p. Player p m => WpPlayer m -> p
于 2011-03-08T18:03:27.713 回答
15

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

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

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

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

于 2011-03-08T17:57:19.810 回答
6

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

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

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

data Useless = exists s. Useless s

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

于 2011-03-08T16:34:10.163 回答
5

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/

于 2011-03-08T17:50:00.903 回答