Je commence à comprendre comment le forallmot-clé est utilisé dans les soi-disant "types existentiels" comme ceci:

data ShowBox = forall s. Show s => SB s

Ce n'est qu'un sous-ensemble, cependant, de la façon dont il forallest utilisé et je ne peux tout simplement pas me concentrer sur son utilisation dans des choses comme ceci:

runST :: forall a. (forall s. ST s a) -> a

Ou en expliquant pourquoi ceux-ci sont différents:

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

Ou tout RankNTypesça ...

J'ai tendance à préférer un anglais clair et sans jargon plutôt que les types de langue qui sont normaux dans les environnements académiques. La plupart des explications que j'essaie de lire à ce sujet (celles que je peux trouver via les moteurs de recherche) ont ces problèmes:

1. Ils sont incomplets. Ils expliquent une partie de l'utilisation de ce mot-clé (comme "types existentiels") qui me fait plaisir jusqu'à ce que je lise le code qui l'utilise d'une manière complètement différente (comme runST, fooet barau - dessus).
2. Ils sont densément chargés d'hypothèses selon lesquelles j'ai lu la dernière en date dans n'importe quelle branche des mathématiques discrètes, de la théorie des catégories ou de l'algèbre abstraite populaire cette semaine. (Si je ne lis jamais les mots « consulter le papier tout pour les détails de la mise en œuvre » à nouveau, il sera trop tôt.)
3. Ils sont écrits d'une manière qui transforme souvent même des concepts simples en grammaire et sémantique tortueusement tordues et fracturées.

Alors...

Passons à la vraie question. Quelqu'un peut-il expliquer complètement le forallmot - clé dans un anglais clair et simple (ou, s'il existe quelque part, indiquer une explication aussi claire que j'ai ratée) qui ne suppose pas que je suis un mathématicien imprégné de jargon?

Modifié pour ajouter:

Il y avait deux réponses remarquables parmi celles de meilleure qualité ci-dessous, mais malheureusement, je ne peux en choisir qu'une comme meilleure. La réponse de Norman était détaillée et utile, expliquant les choses d'une manière qui montrait certains des fondements théoriques forallet en même temps me montrait certaines de ses implications pratiques. la réponse de yairchua couvert un domaine que personne d'autre n'a mentionné (variables de type de portée) et a illustré tous les concepts avec du code et une session GHCi. S'il était possible de sélectionner les deux au mieux, je le ferais. Malheureusement, je ne peux pas et, après avoir examiné attentivement les deux réponses, j'ai décidé que le yairchu borde légèrement celui de Norman en raison du code illustratif et des explications jointes. C'est un peu injuste, cependant, car j'avais vraiment besoin des deux réponses pour comprendre cela au point que forallcela ne me laisse pas un faible sentiment de crainte quand je le vois dans une signature de type.

Commençons par un exemple de code:

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

Ce code ne compile pas (erreur de syntaxe) dans Haskell 98 simple. Il nécessite une extension pour prendre en charge le forallmot - clé.

Au fond, il y a 3 différentes utilisations communes pour le forallmot - clé (ou au moins il semble ), et chacun a sa propre extension Haskell: ScopedTypeVariables, RankNTypes/ Rank2Types, ExistentialQuantification.

Le code ci-dessus n'obtient pas d'erreur de syntaxe avec l'un ou l'autre de ceux activés, mais vérifie uniquement le type avec ScopedTypeVariablesactivé.

Variables de type étendues:

Les variables de type étendues permettent de spécifier les types de code à l'intérieur des whereclauses. Il fait le bdans val :: ble même que l' ben foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b.

Un point déroutant : vous pouvez entendre que lorsque vous omettez le foralltype, il est en fait toujours implicitement là. (d' après la réponse de Norman: "normalement ces langages omettent le forall des types polymorphes" ). Cette affirmation est correcte, mais elle se réfère aux autres utilisations forallet non à l' ScopedTypeVariablesutilisation.

Rang-N-Types:

Commençons par cela mayb :: b -> (a -> b) -> Maybe a -> best équivalent à mayb :: forall a b. b -> (a -> b) -> Maybe a -> b, sauf quand ScopedTypeVariablesest activé.

Cela signifie que cela fonctionne pour tous aet b.

Disons que vous voulez faire quelque chose comme ça.

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

Quel doit être le type de cela liftTup? Ça l'est liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b). Pour voir pourquoi, essayons de le coder:

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

"Hmm .. pourquoi GHC infère-t-il que le tuple doit contenir deux du même type? Disons-le qu'ils ne doivent pas être"

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

Hmm. donc ici GHC ne nous laisse pas appliquer liftFuncsur vcar v :: bet liftFuncveut un x. Nous voulons vraiment que notre fonction obtienne une fonction qui accepte tout possible x!

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

Ce n'est donc pas ce liftTupqui fonctionne pour tous x, c'est la fonction qu'il obtient qui le fait.

Quantification existentielle:

Prenons un exemple:

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

En quoi est-ce différent des Rank-N-Types?

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

Avec Rank-N-Types, cela forall asignifie que votre expression doit correspondre à tous les possibles a. Par exemple:

ghci> length ([] :: forall a. [a])
0

Une liste vide fonctionne comme une liste de tout type.

Donc, avec Existential-Quantification, foralls dans les datadéfinitions signifie que la valeur contenue peut être de n'importe quel type approprié, pas qu'elle doit être de tous les types appropriés.

Quelqu'un peut-il expliquer complètement le mot-clé forall dans un anglais clair et simple?

Non. (Peut-être que Don Stewart le peut.)

Voici les obstacles à une explication simple et claire ou forall:

• C'est un quantificateur. Vous devez avoir au moins un peu de logique (calcul des prédicats) pour avoir vu un quantificateur universel ou existentiel. Si vous n'avez jamais vu de calcul de prédicat ou que vous n'êtes pas à l'aise avec les quantificateurs (et que j'ai vu des étudiants lors des examens de qualification de doctorat qui ne sont pas à l'aise), alors pour vous, il n'y a pas d'explication facile forall.

• C'est un quantificateur de type . Si vous n'avez pas vu System F et que vous avez appris à écrire des types polymorphes, vous allez trouver forallconfus. L'expérience avec Haskell ou ML n'est pas suffisante, car normalement ces langages omettent les foralltypes polymorphes. (Dans mon esprit, c'est une erreur de conception du langage.)

• Dans Haskell en particulier, il forallest utilisé d'une manière que je trouve confuse. (Je ne suis pas un théoricien des types, mais mon travail me met en contact avec beaucoup de théorie des types, et je suis assez à l'aise avec elle.) Pour moi, la principale source de confusion est celle forallutilisée pour coder un type qui Je préférerais moi-même écrire avec exists. Il est justifié par un peu délicat d'isomorphisme de type impliquant des quantificateurs et des flèches, et chaque fois que je veux le comprendre, je dois rechercher les choses et déterminer l'isomorphisme moi-même.

  Si vous n'êtes pas à l'aise avec l'idée d'isomorphisme de type, ou si vous n'avez aucune pratique de réflexion sur les isomorphismes de type, cette utilisation de forallva vous contrarier.

• Bien que le concept général de forallsoit toujours le même (contraignant pour introduire une variable de type), les détails des différentes utilisations peuvent varier considérablement. L'anglais informel n'est pas un très bon outil pour expliquer les variations. Pour vraiment comprendre ce qui se passe, vous avez besoin de quelques mathématiques. Dans ce cas, les mathématiques pertinentes peuvent être trouvées dans le texte d'introduction Types et langages de programmation de Benjamin Pierce , qui est un très bon livre.

Quant à vos exemples particuliers,

• runST devrait vous faire mal à la tête. Les types de rang supérieur (tout à gauche d'une flèche) sont rarement trouvés dans la nature. Je vous encourage à lire l'article qui a présenté runST: "Threads d'état fonctionnel paresseux" . C'est un très bon article, et il vous donnera une bien meilleure intuition pour le type runSTen particulier et pour les types de rang supérieur en général. L'explication prend plusieurs pages, c'est très bien fait, et je ne vais pas essayer de la condenser ici.

• Considérer

  foo :: (forall a. a -> a) -> (Char,Bool)
  bar :: forall a. ((a -> a) -> (Char, Bool))
  

  Si j'appelle bar, je peux simplement choisir n'importe quel type aque j'aime, et je peux lui passer une fonction de type aen type a. Par exemple, je peux passer la fonction (+1)ou la fonction reverse. Vous pouvez penser au forallcomme disant "je peux choisir le type maintenant". (Le mot technique pour choisir le type est instanciant .)

  Les restrictions à l'appel foosont beaucoup plus strictes: l'argument to foo doit être une fonction polymorphe. Avec ce type, les seules fonctions auxquelles je peux passer foosont idou une fonction qui diverge toujours ou des erreurs, comme undefined. La raison en est qu'avec foo, le forallest à gauche de la flèche, donc comme l'appelant de fooje ne peux pas choisir ce qui aest - c'est plutôt l' implémentation de foocela qui permet de choisir ce qui aest. Parce que forallc'est à gauche de la flèche, plutôt qu'au-dessus de la flèche comme dans bar, l'instanciation a lieu dans le corps de la fonction plutôt qu'au niveau du site d'appel.

Résumé: Une explication complète du forallmot - clé nécessite des mathématiques et ne peut être comprise que par une personne qui a étudié les mathématiques. Même les explications partielles sont difficiles à comprendre sans mathématiques. Mais peut-être que mes explications partielles non mathématiques aident un peu. Allez lire Launchbury et Peyton Jones sur runST!

Addendum: jargon "au-dessus", "en dessous", "à gauche de". Ceux-ci n'ont rien à voir avec la façon dont les types textuels sont écrits et tout à voir avec les arbres de syntaxe abstraite. Dans la syntaxe abstraite, a forallprend le nom d'une variable de type, puis il y a un type complet "sous" le forall. Une flèche prend deux types (argument et type de résultat) et forme un nouveau type (le type de fonction). Le type d'argument est "à gauche de" la flèche; c'est l'enfant gauche de la flèche dans l'arbre de syntaxe abstraite.

Exemples:

• Dans forall a . [a] -> [a], le forall est au-dessus de la flèche; ce qui est à gauche de la flèche [a].

• Dans

  forall n f e x . (forall e x . n e x -> f -> Fact x f) 
                -> Block n e x -> f -> Fact x f
  

  le type entre parenthèses serait appelé "un forall à gauche d'une flèche". (J'utilise des types comme celui-ci dans un optimiseur sur lequel je travaille.)

Ma réponse originale:

Quelqu'un peut-il expliquer complètement le mot-clé forall en anglais clair et simple

Comme Norman l'indique, il est très difficile de donner une explication claire et simple en anglais d'un terme technique issu de la théorie des types. Nous essayons tous cependant.

Il n'y a vraiment qu'une chose à retenir à propos de 'forall': il lie les types à une certaine portée . Une fois que vous comprenez cela, tout est assez facile. C'est l'équivalent de «lambda» (ou une forme de «let») au niveau du type - Norman Ramsey utilise la notion de «gauche» / «au-dessus» pour transmettre ce même concept de portée dans son excellente réponse .

La plupart des utilisations de 'forall' sont très simples, et vous pouvez les trouver introduites dans le manuel d'utilisation du GHC, S7.8 ., En particulier l'excellent S7.8.5 sur les formes imbriquées de 'forall'.

Dans Haskell, nous laissons généralement le classeur pour les types, lorsque le type est universellement quanitifié, comme ceci:

length :: forall a. [a] -> Int

est équivalent à:

length :: [a] -> Int

C'est tout.

Comme vous pouvez désormais lier des variables de type à une certaine étendue, vous pouvez avoir des étendues autres que le niveau supérieur (" universellement quantifié "), comme votre premier exemple, où la variable de type n'est visible que dans la structure de données. Cela permet des types cachés (" types existentiels "). Ou nous pouvons avoir une imbrication arbitraire des liaisons ("types N de rang").

Pour comprendre en profondeur les systèmes de types, vous devrez apprendre un peu de jargon. C'est la nature de l'informatique. Cependant, des utilisations simples, comme ci-dessus, devraient pouvoir être saisies intuitivement, par analogie avec «let» au niveau de la valeur. Launchbury et Peyton Jones sont une excellente introduction .

Ils sont densément chargés d'hypothèses selon lesquelles j'ai lu la dernière en date dans n'importe quelle branche des mathématiques discrètes, de la théorie des catégories ou de l'algèbre abstraite qui est populaire cette semaine. (Si je ne relis jamais les mots "consultez le document pour des détails de mise en œuvre", ce sera trop tôt.)

Euh, et qu'en est-il de la logique simple du premier ordre? forallest assez clairement en référence à la quantification universelle , et dans ce contexte, le terme existentiel a également plus de sens, bien qu'il serait moins gênant s'il y avait un existsmot-clé. Que la quantification soit effectivement universelle ou existentielle dépend du placement du quantificateur par rapport à l'endroit où les variables sont utilisées de quel côté d'une flèche de fonction et tout cela est un peu déroutant.

Donc, si cela n'aide pas ou si vous n'aimez tout simplement pas la logique symbolique, d'un point de vue de programmation plus fonctionnel, vous pouvez considérer les variables de type comme étant simplement des paramètres de type (implicites) pour la fonction. Les fonctions prenant des paramètres de type dans ce sens sont traditionnellement écrites en utilisant un lambda majuscule pour une raison quelconque, que j'écrirai ici comme /\.

Considérez donc la idfonction:

id :: forall a. a -> a
id x = x

Nous pouvons le réécrire en lambdas, en déplaçant le "paramètre type" de la signature de type et en ajoutant des annotations de type en ligne:

id = /\a -> (\x -> x) :: a -> a

Voici la même chose que pour const:

const = /\a b -> (\x y -> x) :: a -> b -> a

Votre barfonction pourrait donc ressembler à ceci:

bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)

Notez que le type de la fonction donnée baren argument dépend du barparamètre type de. Considérez si vous aviez quelque chose comme ça à la place:

bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool)

Voici l' bar2application de la fonction à quelque chose de type Char, donc donner bar2tout paramètre de type autre que Charprovoquera une erreur de type.

D'un autre côté, voici à quoi cela foopourrait ressembler:

foo = (\f -> (f Char 't', f Bool True))

Contrairement à bar, foone prend aucun paramètre de type! Il prend une fonction qui prend elle - même un paramètre de type, puis applique cette fonction à deux types différents .

Ainsi, lorsque vous voyez un foralldans une signature de type, pensez-y simplement comme une expression lambda pour les signatures de type . Tout comme les lambdas réguliers, la portée de foralls'étend aussi loin que possible vers la droite, jusqu'à la parenthèse englobante, et tout comme les variables liées dans une lambda régulière, les variables de type liées par a forallne sont dans la portée que dans l'expression quantifiée.

Post scriptum : Vous vous demandez peut-être - maintenant que nous pensons à des fonctions prenant des paramètres de type, pourquoi ne pouvons-nous pas faire quelque chose de plus intéressant avec ces paramètres que de les mettre dans une signature de type? La réponse est que nous pouvons!

Une fonction qui associe des variables de type à une étiquette et renvoie un nouveau type est un constructeur de type , que vous pourriez écrire quelque chose comme ceci:

Either = /\a b -> ...

Mais nous aurions besoin d'une notation complètement nouvelle, car la façon dont un tel type est écrit, comme Either a b, suggère déjà «d'appliquer la fonction Eitherà ces paramètres».

D'un autre côté, une fonction qui sorte de "modèle de correspondance" sur ses paramètres de type, renvoyant des valeurs différentes pour différents types, est une méthode d'une classe de type . Une légère expansion de ma /\syntaxe ci-dessus suggère quelque chose comme ceci:

fmap = /\ f a b -> case f of
    Maybe -> (\g x -> case x of
        Just y -> Just b g y
        Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b
    [] -> (\g x -> case x of
        (y:ys) -> g y : fmap [] a b g ys 
        []     -> [] b) :: (a -> b) -> [a] -> [b]

Personnellement, je pense que je préfère la syntaxe réelle de Haskell ...

Une fonction qui "modèle correspond" à ses paramètres de type et renvoie un type arbitraire existant est une famille de types ou une dépendance fonctionnelle - dans le premier cas, elle ressemble déjà beaucoup à une définition de fonction.

Voici une explication rapide et grossière en termes simples que vous connaissez probablement déjà.

Le forallmot-clé n'est vraiment utilisé que d'une seule façon dans Haskell. Cela signifie toujours la même chose quand vous le voyez.

Quantification universelle

Un type universellement quantifié est un type de formulaire forall a. f a. Une valeur de ce type peut être considérée comme une fonction qui prend un type a comme argument et renvoie une valeur de type f a. Sauf que dans Haskell ces arguments de type sont passés implicitement par le système de type. Cette "fonction" doit vous donner la même valeur quel que soit le type qu'elle reçoit, donc la valeur est polymorphe .

Par exemple, considérez le type forall a. [a]. Une valeur de ce type prend un autre type aet vous renvoie une liste d'éléments de ce même type a. Il n'y a bien sûr qu'une seule implémentation possible. Il faudrait qu'il vous donne la liste vide car il apourrait être de tout type. La liste vide est la seule valeur de liste polymorphe dans son type d'élément (car elle ne contient aucun élément).

Ou le type forall a. a -> a. L'appelant d'une telle fonction fournit à la fois un type aet une valeur de type a. L'implémentation doit alors retourner une valeur de ce même type a. Il n'y a encore qu'une seule implémentation possible. Il devrait retourner la même valeur que celle qui lui a été donnée.

Quantification existentielle

Un type existentiellement quantifié aurait la forme exists a. f a, si Haskell supportait cette notation. Une valeur de ce type peut être considérée comme une paire (ou un "produit") composé d'un type aet d'une valeur de type f a.

Par exemple, si vous avez une valeur de type exists a. [a], vous avez une liste d'éléments d'un certain type. Il peut s'agir de n'importe quel type, mais même si vous ne savez pas ce que c'est, vous pouvez faire beaucoup de choses sur une telle liste. Vous pouvez l'inverser, ou vous pouvez compter le nombre d'éléments, ou effectuer toute autre opération de liste qui ne dépend pas du type des éléments.

OK, alors attendez une minute. Pourquoi Haskell utilise-t-il forallpour désigner un type "existentiel" comme le suivant?

data ShowBox = forall s. Show s => SB s

Cela peut être déroutant, mais il décrit vraiment le type du constructeur de données SB :

SB :: forall s. Show s => s -> ShowBox

Une fois construite, vous pouvez penser à une valeur de type ShowBoxcomme consistant en deux choses. C'est un type savec une valeur de type s. En d'autres termes, c'est une valeur d'un type existentiellement quantifié. ShowBoxpourrait vraiment être écrit comme exists s. Show s => s, si Haskell supportait cette notation.

runST et amis

Cela étant, en quoi sont-ils différents?

foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

Prenons d'abord bar. Il prend un type aet une fonction de type a -> aet produit une valeur de type (Char, Bool). On pourrait choisir Intcomme le aet lui donner une fonction de type Int -> Intpar exemple. Mais fooc'est différent. Cela nécessite que l'implémentation de foopuisse transmettre tout type qu'il veut à la fonction que nous lui donnons. Donc, la seule fonction que nous pourrions raisonnablement lui donner est id.

Nous devrions maintenant être en mesure d'aborder la signification du type de runST:

runST :: forall a. (forall s. ST s a) -> a

Il runSTfaut donc pouvoir produire une valeur de type a, quel que soit le type que nous donnons a. Pour ce faire, il utilise un argument de type forall s. ST s aqui doit certainement produire le a. De plus, il doit être capable de produire une valeur de type aquel que soit le type d'implémentation de runSTdécide de donner as s.

Okay, alors quoi? L'avantage est que cela impose une contrainte à l'appelant runSTen ce que le type ane peut pas du tout impliquer le type s. Vous ne pouvez pas lui passer une valeur de type ST s [s], par exemple. En pratique, cela signifie que la mise en œuvre de runSTest libre d'effectuer une mutation avec la valeur de type s. Le type garantit que cette mutation est locale à la mise en œuvre de runST.

Le type de runSTest un exemple de type polymorphe de rang 2 car le type de son argument contient un forallquantificateur. Le type de fooci - dessus est de rang 2. Un type polymorphes ordinaire, comme celui de bar, est de rang 1, mais il devient de rang 2 si les types d'arguments doivent être polymorphes, avec leur propre forallquantificateurs. Et si une fonction prend des arguments de rang 2, son type est de rang 3, etc. En général, un type qui prend des arguments polymorphes de rang na rang n + 1.

Quelqu'un peut-il expliquer complètement le mot clé forall dans un anglais clair et simple (ou, s'il existe quelque part, indiquer une explication aussi claire que j'ai ratée) qui ne suppose pas que je suis un mathématicien imprégné de jargon?

Je vais essayer d'expliquer juste le sens et peut-être l'application de foralldans le contexte de Haskell et de ses systèmes de types.

Mais avant de comprendre que je voudrais vous diriger vers un discours très accessible et agréable par Runar Bjarnason intitulé « Contraintes Liberate, des libertés Contraindre ». L'exposé est plein d'exemples tirés de cas d'utilisation du monde réel ainsi que d'exemples dans Scala pour soutenir cette déclaration, bien qu'il ne le mentionne pas forall. Je vais essayer d'expliquer la forallperspective ci-dessous.

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

Il est très important de digérer et de croire cette déclaration pour continuer avec l'explication suivante, donc je vous invite à regarder la conférence (au moins une partie de celle-ci).

Maintenant, un exemple très courant, montrant l’expressivité du système de type Haskell est cette signature de type:

foo :: a -> a

On dit qu'étant donné ce type de signature, il n'y a qu'une seule fonction qui peut satisfaire ce type et qui est la identityfonction ou ce qui est plus connu id.

Au début de mon apprentissage de Haskell, je me suis toujours demandé les fonctions ci-dessous:

foo 5 = 6

foo True = False

ils satisfont tous les deux à la signature de type ci-dessus, alors pourquoi les gens de Haskell affirment que c'est idseul qui satisfait la signature de type?

C'est parce qu'il y a un implicite forallcaché dans la signature de type. Le type réel est:

id :: forall a. a -> a

Alors, revenons maintenant à la déclaration: les contraintes libèrent, les libertés contraignent

En traduisant cela dans le système de type, cette déclaration devient:

Une contrainte au niveau du type, devient une liberté au niveau du terme

et

Une liberté au niveau du type, devient une contrainte au niveau du terme

Essayons de prouver la première affirmation:

Une contrainte au niveau du type.

Donc, mettre une contrainte sur notre signature de type

foo :: (Num a) => a -> a

devient une liberté au niveau du terme nous donne la liberté ou la flexibilité d'écrire tous ces

foo 5 = 6
foo 4 = 2
foo 7 = 9
...

La même chose peut être observée en contraignant aavec toute autre classe de type, etc.

Alors maintenant, ce que cette signature de type: se foo :: (Num a) => a -> atraduit par:

∃a , st a -> a, ∀a ∈ Num

Ceci est connu sous le nom de quantification existentielle, ce qui signifie qu'il existe des instances apour lesquelles une fonction, lorsqu'elle est alimentée par quelque chose de type, arenvoie quelque chose du même type, et ces instances appartiennent toutes à l'ensemble des nombres.

Par conséquent, nous pouvons voir l'ajout d'une contrainte (qui adevrait appartenir à l'ensemble de nombres), libère le niveau de terme pour avoir plusieurs implémentations possibles.

Venons-en maintenant à la deuxième déclaration et celle qui porte en fait l'explication de forall:

Une liberté au niveau du type, devient une contrainte au niveau du terme

Libérons maintenant la fonction au niveau du type:

foo :: forall a. a -> a

Maintenant, cela se traduit par:

∀a , a -> a

ce qui signifie que la mise en œuvre de ce type de signature doit être telle qu'elle l'est a -> aen toutes circonstances.

Alors maintenant, cela commence à nous contraindre au niveau du terme. On ne peut plus écrire

foo 5 = 7

car cette implémentation ne satisferait pas si on la mettait en atant que Bool. apeut être un Charou un [Char]ou un type de données personnalisé. Dans tous les cas, il doit renvoyer quelque chose du même type. Cette liberté au niveau du type est ce qu'on appelle la quantification universelle et la seule fonction qui peut y répondre est

foo a = a

qui est communément appelé la identityfonction

Il en résulte forallun libertyniveau au niveau du type, dont le but réel est au constrainniveau du terme pour une implémentation particulière.

La raison pour laquelle il existe différentes utilisations de ce mot-clé est qu'il est en fait utilisé dans au moins deux extensions système de types différents: les types de rang supérieur et les existentiels.

Il est probablement préférable de lire et de comprendre ces deux choses séparément, plutôt que d'essayer d'obtenir une explication de la raison pour laquelle `` forall '' est un bit de syntaxe approprié dans les deux en même temps.

Comment est existentiel existentiel?

Avec Existential-Quantification, foralls dans les datadéfinitions signifie que la valeur contenue peut être de n'importe quel type approprié, pas qu'elle doit être de tous les types appropriés. - la réponse de yachiru

Une explication de la raison forallpour laquelle les datadéfinitions sont isomorphes à (exists a. a)(pseudo-Haskell) peut être trouvée dans les "Haskell / Existentialement quantified types" de wikibooks .

Voici un bref résumé textuel:

data T = forall a. MkT a -- an existential datatype
MkT :: forall a. a -> T -- the type of the existential constructor

Lors du filtrage / déconstruction de modèles MkT x, quel est le type de x?

foo (MkT x) = ... -- -- what is the type of x?

xpeut être de n'importe quel type (comme indiqué dans le forall), et son type est donc:

x :: exists a. a -- (pseudo-Haskell)

Par conséquent, les éléments suivants sont isomorphes:

data T = forall a. MkT a -- an existential datatype
data T = MkT (exists a. a) -- (pseudo-Haskell)

forall signifie forall

Ma simple interprétation de tout cela, c'est que " forallsignifie vraiment" pour tous "". Une distinction importante à faire est l'impact de forallsur la définition par rapport à l' application de fonction .

A forallsignifie que la définition de la valeur ou de la fonction doit être polymorphe.

Si la chose définie est une valeur polymorphe , cela signifie que la valeur doit être valable pour tous les éléments appropriés a, ce qui est assez restrictif.

Si la chose définie est une fonction polymorphe , cela signifie que la fonction doit être valide pour toutes les personnes appropriées a, ce qui n'est pas si restrictif parce que le fait que la fonction soit polymorphe ne signifie pas que le paramètre appliqué doit être polymorphe. Autrement dit, si la fonction est valable pour tous a, à l'inverse, n'importe quelle convenance apeut être appliquée à la fonction. Cependant, le type du paramètre ne peut être choisi qu'une seule fois dans la définition de la fonction.

Si a se foralltrouve à l'intérieur du type du paramètre de fonction (c'est-à-dire a Rank2Type), cela signifie que le paramètre appliqué doit être vraiment polymorphe, pour être cohérent avec l'idée forallque la définition des moyens est polymorphe. Dans ce cas, le type du paramètre peut être choisi plusieurs fois dans la définition de la fonction ( "et est choisi par l'implémentation de la fonction", comme le souligne Norman )

Par conséquent, la raison pour laquelle les datadéfinitions existentielles autorisent tout a est parce que le constructeur de données est une fonction polymorphe :

MkT :: forall a. a -> T

sorte de MkT :: a -> *

Ce qui signifie que n'importe laquelle apeut être appliquée à la fonction. Par opposition à, disons, une valeur polymorphe :

valueT :: forall a. [a]

type de valeurT :: a

Ce qui signifie que la définition de valueT doit être polymorphe. Dans ce cas, valueTpeut être défini comme une liste vide []de tous les types.

[] :: [t]

Différences

Même si la signification de forallest cohérente dans ExistentialQuantificationet RankNType, les existentielles ont une différence puisque le dataconstructeur peut être utilisé dans la correspondance de motifs. Comme indiqué dans le guide de l'utilisateur ghc :

Lors de la correspondance de modèle, chaque correspondance de modèle introduit un nouveau type distinct pour chaque variable de type existentiel. Ces types ne peuvent pas être unifiés avec un autre type, ni échapper à la portée de la correspondance de modèle.