Que signifie "existe" dans le système de types Haskell?

Question

J'ai du mal à comprendre l' exists mot-clé par rapport à Haskell type de système. Autant que je sache, il n'existe pas de mot-clé en Haskell par défaut, mais:

• Il y a des extensions qui ajoutent eux, dans des déclarations comme ces data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
• J'ai vu un article sur eux, et (si je me souviens bien), elle a indiqué qu' exists mot-clé n'est pas nécessaire pour le type de système car il peut être généralisée en forall

Mais je ne peux même pas comprendre ce qu' exists moyens.

Quand je dis, forall a . a -> Int, cela signifie (dans ma compréhension, l'incorrect, je suppose) "pour chaque (type) a, il y a une fonction d'un type 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

Quand je dis exists a . a -> Int, que peut-il dire? "Il y a au moins un type a pour lesquels il existe une fonction d'un type a -> Int"? Pourquoi on écrire une telle déclaration? Quel est le but? La sémantique? Comportement du compilateur?

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

Veuillez noter qu'il n'est pas destiné à être un véritable code qui permet de compiler, juste un exemple de ce que je suis en imaginant puis j'ai entendu parler de ces quantificateurs.

J'ai essayé de lire les docs, mais mes faibles compétences en anglais et pauvres compétences en Mathématiques obtenir de la manière, je suppose.

Ça semble être un gros malentendu... Merci de m'aider à l'obtenir droite

---

P. S. je ne suis pas exactement un débutant total en Haskell (peut-être comme une seconde niveleuse), mais mes calculs de fondations de ces choses manquent, donc si vous connaissez une bonne (peut-être compliqué, mais bon et compréhensible sans Doctorat) livre, le papier ou sur le guide, s'il vous plaît me dire à ce sujet

Answer 1

Une utilisation des existentielle types que j'ai couru en est avec mon code pour la médiation d'un jeu de Clue.

Mon médiation sorte de code agit comme un courtier. Il ne se soucie pas de ce que les types de joueurs sont - tous il se soucie est que tous les acteurs de mettre en œuvre les crochets donné dans l' Player typeclass.

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

Maintenant, le concessionnaire pourrait garder une liste de joueurs de type Player p m => [p], mais qui se contractent tous les joueurs sont du même type.

C'est trop contraignant. Que faire si je veux avoir différents types de joueurs, chacun mis en œuvre différemment, et de les exécuter à l'encontre les uns des autres?

J'ai donc utiliser ExistentialTypes pour créer un wrapper pour les joueurs:

-- wrapper for storing a player within a given monad
data WpPlayer m = forall p. Player p m => WpPlayer p

Maintenant je peut facilement garder un caractère hétérogène de la liste des joueurs. Le revendeur peut encore facilement interagir avec le les joueurs à l'aide de l'interface spécifiée par l' Player typeclass.

Prendre en compte le type du constructeur WpPlayer.

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

Autre que le pourtout à l'avant, c'est assez standard haskell. Pour tous les types p qui satisfont le contrat Player p m, le constructeur WpPlayer cartes d'une valeur de type p à une valeur de type WpPlayer m.

Le morceau intéressant est livré avec un déconstructeur:

    unWpPlayer (WpPlayer p) = p

Quel est le type d' unWpPlayer? Ce travail?

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

Non, pas vraiment. Un tas de différents types de p pourrait satisfaire l' Player p mcontrat avec un type particulier m. Et nous avons donné l' WpPlayer constructeur un particulier de type p, de sorte qu'il doit renvoyer le même type. On ne peut donc pas utiliser forall.

Tout ce que nous pouvons vraiment dire, c'est qu'il existe un certain type p, ce qui répond à l' Player p mcontrat avec le type m.

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

Answer 2

Quand je dis, pourtout un . a -> Int, il des moyens (dans ma compréhension, l' incorrect, je suppose) "pour tous les (type a), il existe une fonction d'une type a -> Int":

Presque, mais pas tout à fait. Il signifie "pour chaque type a, cette fonction peut être considérée comme de type a -> Int. Donc, a peuvent être spécialisés pour n'importe quel type de l'appelant de choisir.

Dans le "il existe" un cas, nous avons: "certains (en particulier, mais inconnu) de type a, de sorte que cette fonction est du type a -> Int. Donc, a doit être un type spécifique, mais l'appelant ne sais pas quoi.

Notez que cela signifie que ce type particulier (exists a. a -> Int) n'a pas grand intérêt - il n'y a pas moyen utile d'appeler cette fonction sauf à passer un "bas" valeur tels que l' undefined ou let x = x in x. Plus utile, la signature pourrait être exists a. Foo a => Int -> a. Il est dit que la fonction renvoie un type spécifique a, mais vous n'obtenez pas de savoir de quel type. Mais vous savez que c'est un exemple d' Foo - de sorte que vous pouvez faire quelque chose d'utile avec elle, en dépit de ne pas connaître son "true type".

Answer 3

Il signifie précisément "il existe un type a pour qui je peut fournir des valeurs des types suivants dans mon constructeur". Notez que ceci est différent de dire "la valeur de a est Int dans mon constructeur"; dans le dernier cas, je sais ce que le type est, et j'ai pu utiliser mon propre fonction qui prend Ints comme arguments à faire quelque chose d'autre pour les valeurs du type de données.

Ainsi, du point de vue pragmatique, existentielle types vous permettent de masquer le type sous-jacent dans une structure de données, de forcer le programmeur à utiliser uniquement les opérations que vous avez défini. Il représente l'encapsulation.

C'est pour cette raison que ce type n'est pas très utile:

data Useless = exists s. Useless s

Car il n'y a rien que je peux faire pour la valeur (pas tout à fait vrai; je pourrais seq il); je ne sais rien à propos de son type.

Answer 4

CHU met en œuvre le mot-clé existe. Voici un exemple de la documentation

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

Et un autre:

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 provoque une erreur de type. Cependant, nous pouvons utiliser y1 et y2 parfaitement bien:"

main :: IO ()
main = do putStrLn (show (xapp y1))
          putStrLn (show (xapp y2))

ezyang aussi blogué bien à ce sujet: http://blog.ezyang.com/2010/10/existential-type-curry/