Clarification sur les types existentiels dans Haskell

J'essaie de comprendre les types existentiels dans Haskell et je suis tombé sur un PDF http://www.ii.uni.wroc.pl/~dabi/courses/ZPF15/rlasocha/prezentacja.pdf

Veuillez corriger mes compréhensions ci-dessous que j'ai jusqu'à présent.

• Les types existentiels ne semblent pas être intéressés par le type qu'ils contiennent, mais les modèles qui les correspondent disent qu'il existe un type, nous ne savons pas de quel type il s'agit tant que nous n'utilisons pas Typeable ou Data.
• Nous les utilisons lorsque nous voulons masquer des types (ex: pour les listes hétérogènes) ou nous ne savons pas vraiment quels types au moment de la compilation.
• GADT« s fournissent la claire et une meilleure syntaxe au code en utilisant des types existentiels en fournissant implicites forall» s

Mes doutes

• Dans la page 20 du PDF ci-dessus, il est mentionné pour le code ci-dessous qu'il est impossible pour une fonction d'exiger un tampon spécifique. Pourquoi en est-il ainsi? Quand je rédige une fonction, je sais exactement quel type de tampon je vais utiliser même si je ne sais pas quelles données je vais y mettre. Qu'est-ce qui ne va pas? :: Worker MemoryBuffer IntS'ils veulent vraiment faire un résumé sur Buffer, ils peuvent avoir un type Sum data Buffer = MemoryBuffer | NetBuffer | RandomBufferet avoir un type comme:: Worker Buffer Int

data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

• Comme Haskell est un langage d'effacement de type complet comme C, alors comment sait-il au Runtime quelle fonction appeler. Est-ce quelque chose comme si nous allions conserver peu d'informations et passer dans une énorme V-Table de fonctions et au moment de l'exécution, cela va sortir de V-Table? Si tel est le cas, quel type d'informations va-t-il stocker?

Les GADT fournissent la syntaxe claire et meilleure pour coder en utilisant les types existentiels en fournissant des for implicites

Je pense qu'il est généralement admis que la syntaxe GADT est meilleure. Je ne dirais pas que c'est parce que les GADT fournissent des foralls implicites, mais plutôt parce que la syntaxe originale, activée avec l' ExistentialQuantificationextension, est potentiellement déroutante / trompeuse. Cette syntaxe, bien sûr, ressemble à:

data SomeType = forall a. SomeType a

ou avec une contrainte:

data SomeShowableType = forall a. Show a => SomeShowableType a

et je pense que le consensus est que l'utilisation du mot-clé forallici permet de confondre facilement le type avec le type complètement différent:

data AnyType = AnyType (forall a. a)    -- need RankNTypes extension

Une meilleure syntaxe aurait pu utiliser un existsmot-clé distinct , vous écririez donc:

data SomeType = SomeType (exists a. a)   -- not valid GHC syntax

La syntaxe GADT, qu'elle soit utilisée avec implicite ou explicite forall, est plus uniforme entre ces types et semble plus facile à comprendre. Même avec un explicite forall, la définition suivante passe à travers l'idée que vous pouvez prendre une valeur de n'importe quel type aet la mettre dans un monomorphe SomeType':

data SomeType' where
    SomeType' :: forall a. (a -> SomeType')   -- parentheses optional

et il est facile de voir et de comprendre la différence entre ce type et:

data AnyType' where
    AnyType' :: (forall a. a) -> AnyType'

Les types existentiels ne semblent pas être intéressés par le type qu'ils contiennent, mais les modèles qui les correspondent disent qu'il existe un type, nous ne savons pas de quel type il s'agit tant que nous n'utilisons pas Typeable ou Data.

Nous les utilisons lorsque nous voulons masquer des types (ex: pour les listes hétérogènes) ou nous ne savons pas vraiment quels types au moment de la compilation.

Je suppose que ce n'est pas trop loin, bien que vous n'ayez pas à utiliser Typeableou Dataà utiliser des types existentiels. Je pense qu'il serait plus précis de dire qu'un type existentiel fournit une "boîte" bien typée autour d'un type non spécifié. La boîte "cache" le type dans un sens, ce qui vous permet de faire une liste hétérogène de ces boîtes, en ignorant les types qu'elles contiennent. Il s'avère qu'un existentiel non contraint, comme SomeType'ci-dessus, est assez inutile, mais un type contraint:

data SomeShowableType' where
    SomeShowableType' :: forall a. (Show a) => a -> SomeShowableType'

vous permet de faire correspondre les motifs pour jeter un œil à l'intérieur de la "boîte" et de rendre les installations de classe de type disponibles:

showIt :: SomeShowableType' -> String
showIt (SomeShowableType' x) = show x

Notez que cela fonctionne pour n'importe quelle classe de type, pas seulement Typeableou Data.

En ce qui concerne votre confusion à propos de la page 20 du diaporama, l'auteur dit qu'il est impossible pour une fonction qui prend un existentiel Worker d'exiger d' Workeravoir une Bufferinstance particulière . Vous pouvez écrire une fonction pour créer un en Workerutilisant un type particulier de Buffer, comme MemoryBuffer:

class Buffer b where
  output :: String -> b -> IO ()
data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer
instance Buffer MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

mais si vous écrivez une fonction qui prend un Workerargument as, elle ne peut utiliser que les Bufferinstallations de classe de type général (par exemple, la fonction output):

doWork :: Worker Int -> IO ()
doWork (Worker b x) = output (show x) b

Il ne peut pas essayer d'exiger qu'il bs'agisse d'un type particulier de tampon, même via la correspondance de modèles:

doWorkBroken :: Worker Int -> IO ()
doWorkBroken (Worker b x) = case b of
  MemoryBuffer -> error "try this"       -- type error
  _            -> error "try that"

Enfin, les informations d'exécution sur les types existentiels sont mises à disposition via des arguments implicites de "dictionnaire" pour les classes de types impliquées. Le Workertype ci-dessus, en plus d'avoir des champs pour le tampon et l'entrée, a également un champ implicite invisible qui pointe vers le Bufferdictionnaire (un peu comme v-table, bien qu'il soit à peine énorme, car il contient juste un pointeur sur la outputfonction appropriée ).

En interne, la classe de type Bufferest représentée comme un type de données avec des champs de fonction et les instances sont des "dictionnaires" de ce type:

data Buffer' b = Buffer' { output' :: String -> b -> IO () }

dBuffer_MemoryBuffer :: Buffer' MemoryBuffer
dBuffer_MemoryBuffer = Buffer' { output' = undefined }

Le type existentiel a un champ caché pour ce dictionnaire:

data Worker' x = forall b. Worker' { dBuffer :: Buffer' b, buffer' :: b, input' :: x }

et une fonction comme doWorkcelle qui opère sur des Worker'valeurs existentielles est implémentée comme:

doWork' :: Worker' Int -> IO ()
doWork' (Worker' dBuf b x) = output' dBuf (show x) b

Pour une classe de type avec une seule fonction, le dictionnaire est en fait optimisé pour un nouveau type, donc dans cet exemple, le Workertype existentiel inclut un champ caché qui se compose d'un pointeur de fonction vers la outputfonction du tampon, et c'est la seule information d'exécution nécessaire par doWork.

Dans la page 20 du PDF ci-dessus, il est mentionné pour le code ci-dessous qu'il est impossible pour une fonction d'exiger un tampon spécifique. Pourquoi en est-il ainsi?

Parce que Worker, tel que défini, ne prend qu'un seul argument, le type du champ "input" (variable de type x). Par exemple, Worker Intc'est un type. La variable de type b, au contraire, n'est pas un paramètre de Worker, mais est une sorte de "variable locale", pour ainsi dire. Il ne peut pas être transmis comme dans Worker Int String- cela déclencherait une erreur de type.

Si nous définissions plutôt:

data Worker x b = Worker {buffer :: b, input :: x}

fonctionnerait alors Worker Int String, mais le type n'est plus existentiel - nous devons maintenant toujours passer le type de tampon également.

Comme Haskell est un langage d'effacement de type complet comme C, alors comment sait-il au Runtime quelle fonction appeler. Est-ce quelque chose comme si nous allions conserver peu d'informations et passer dans une énorme V-Table de fonctions et au moment de l'exécution, cela va sortir de V-Table? Si tel est le cas, quel type d'informations va-t-il stocker?

C'est à peu près correct. En bref, chaque fois que vous appliquez le constructeur Worker, GHC déduit le btype à partir des arguments de Worker, puis recherche une instance Buffer b. Si cela est trouvé, GHC inclut un pointeur supplémentaire vers l'instance dans l'objet. Dans sa forme la plus simple, ce n'est pas trop différent du "pointeur vers vtable" qui est ajouté à chaque objet dans la POO lorsque des fonctions virtuelles sont présentes.

Dans le cas général, cela peut cependant être beaucoup plus complexe. Le compilateur peut utiliser une représentation différente et ajouter plus de pointeurs au lieu d'une seule (par exemple, en ajoutant directement les pointeurs à toutes les méthodes d'instance), si cela accélère le code. De plus, le compilateur doit parfois utiliser plusieurs instances pour satisfaire une contrainte. Par exemple, si nous devons stocker l'instance pour Eq [Int]... alors il n'y en a pas un mais deux: un pour Intet un pour les listes, et les deux doivent être combinés (au moment de l'exécution, sauf optimisations).

Il est difficile de deviner exactement ce que fait GHC dans chaque cas: cela dépend d'une tonne d'optimisations qui pourraient ou non se déclencher.

Vous pouvez essayer de rechercher sur Google l'implémentation "basée sur un dictionnaire" des classes de types pour en savoir plus sur ce qui se passe. Vous pouvez également demander à GHC d'imprimer le Core optimisé interne -ddump-simplet d'observer les dictionnaires en cours de construction, de stockage et de transmission. Je dois vous avertir: le noyau est plutôt bas, et peut être difficile à lire au début.