34

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「型の関数がある型が少なくとも 1 つある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 の完全な初心者ではありませんが (おそらく 2 年生のように)、これらのことに関する数学の基礎が欠けています。

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 です。contract を満たすすべての型 p についてPlayer p m、コンストラクターは type の値WpPlayerを type の値にマップします。pWpPlayer m

興味深いのは、デコンストラクターです。

    unWpPlayer (WpPlayer p) = p

の種類はunWpPlayer何ですか? これは機能しますか？

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

いいえ、そうではありません。さまざまなタイプの束が、特定の type との契約をp満たすことができます。そして、コンストラクターに特定の型 p を与えたので、同じ型を返す必要があります。したがって、使用できません。Player p mmWpPlayerforall

本当に言えることは、型 との契約を満たす何らかの型 pが存在するということだけです。Player p mm

    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 -> Int を持つような (特定の、しかし不明な) 型 a がいくつかあります」。したがってa、特定の型である必要がありますが、呼び出し元にはわかりません。

これは、この特定の型 ( ) がそれほど興味深いものではないことを意味することに注意してください。またはexists a. a -> Intなどの「底」の値を渡す以外に、その関数を呼び出す便利な方法はありません。より便利な署名は. 関数が特定の型を返すと書かれていますが、どの型かはわかりません。しかし、それがのインスタンスであることは知っているので、その「真の」型を知らなくても、何か役に立つことができます。undefinedlet x = x in xexists a. Foo a => Int -> aaFoo

于 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 に答える