"存在"在Haskell类型系统中意味着什么？

Question

我正在努力理解与existsHaskell类型系统相关的关键字.据我所知,默认情况下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

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

---

PS我不是Haskell的全新手(也许就像二年级学生),但我对这些东西的数学基础缺乏.

Answer 1

我遇到的存在类型的使用是用我的代码来调解线索游戏.

我的调解代码有点像经销商.它并不关心玩家的类型 - 它关心的是所有玩家都实现了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.对于满足合同的所有类型p,Player p m构造函数WpPlayer将type p 的值映射到type 的值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 - > Int,它意味着(在我的理解中,不正确的一个,我猜)"对于每个(类型)a,有一个类型a - > Int"的函数:

关闭,但不完全.它意味着"对于每种类型a,此函数可以被认为具有类型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/