Pourquoi `[1," a "] :: [forall a. Montrer a => a] `n'est pas autorisé?

Question

Dans mon (peut incorrecte) comprendre, après deux listes devraient être équivalentes:

[1, "a"] :: [forall a. Show a => a] 

data V = forall a. Show a => V a 
[V 1, V "a"] :: [V] 

Cependant, le premier n'est pas acceptée, mais la seconde fonctionne très bien (avec ExistentialQuantification).

Si la première liste n'existe pas, quel serait le type dans l'espace vide de map V :: ??? -> [V]? Quel mécanisme de type impose l'existence de l'encapsuleur?

Answer 1

Votre compréhension n'est pas correcte. Une grande partie du problème est que la syntaxe de quantification existentielle traditionnelle que vous avez utilisée est assez confuse pour quiconque ne la connaît pas bien. Je vous recommande donc fortement d'utiliser plutôt la syntaxe GADT, qui a aussi l'avantage d'être strictement plus puissante. La chose facile à faire est simplement d'activer {-# LANGUAGE GADTs #-}. Pendant que nous y sommes, allumons {-# LANGUAGE ScopedTypeVariables #-}, parce que je déteste me demander ce que signifie forall dans un endroit donné. Votre V définition signifie exactement la même chose que

data V where 
    V :: forall a . Show a => a -> V 

On peut effectivement laisser tomber le forall explicite si nous aimons:

data V where 
    V :: Show a => a -> V 

Ainsi, le constructeur de données V est une fonction qui prend quelque chose de toute montrable tapez et produit quelque chose de type V. Le type de map est assez restrictive:

map :: (a -> b) -> [a] -> [b] 

Tous les éléments de la liste transmis à map doivent avoir le même type. Ainsi, le type de map V est juste

map V :: Show a => [a] -> [V] 

Revenons à votre première expression maintenant:

[1, "a"] :: [forall a. Show a => a] 

maintenant ce que cela dit en fait est que [1, "a"] est une liste, dont chacun des éléments a le type forall a . Show a => a. C'est-à-dire, si je fournis une a qui est une instance de Show, chaque élément de la liste devrait avoir ce type. Ce n'est simplement pas vrai. "a" n'a pas, par exemple, le type Bool. Il y a encore un autre problème ici; le type [forall a . Show a => a] est "imprévisible". Je ne comprends pas les détails de ce que cela signifie, mais en gros, vous avez coincé un forall dans l'argument d'un constructeur de type autre que ->, et ce n'est pas autorisé. GHC pourrait vous suggérer d'activer l'extension ImpredicativeTypes, mais cela ne fonctionne vraiment pas, donc vous ne devriez pas. Si vous voulez une liste de choses existentiellement quantifiées, vous devez les inclure d'abord dans des types de données existentiels ou utiliser un type de liste existentielle spécialisé. Si vous voulez une liste de choses universellement quantifiées, vous devez les envelopper d'abord (probablement dans newtypes).