Warum `[1," a "] :: [forall a. Show a => a] `ist nicht erlaubt?

Question

In meinem (möglicherweise falsch) Verständnis, sollten folgende zwei Listen gleichwertig:

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

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

jedoch die erste nicht akzeptiert, aber der zweite funktioniert gut (mit ExistentialQuantification).

Wenn die erste Liste nicht existiert, was wäre der Typ in der Null von map V :: ??? -> [V]? Welcher Typ-Mechanismus erzwingt die Existenz des Wrappers?

Answer 1

Ihr Verständnis ist nicht richtig. Ein großer Teil des Problems besteht darin, dass die traditionelle existenzielle Quantifizierungssyntax, die Sie verwendet haben, ziemlich verwirrend für jeden ist, der sie nicht gründlich kennt. Ich empfehle daher dringend, dass Sie stattdessen die GADT-Syntax verwenden, die auch den Vorteil hat, dass sie strikter ist. Die einfache Möglichkeit ist, nur {-# LANGUAGE GADTs #-} zu aktivieren. Während wir dabei sind, schalten wir {-# LANGUAGE ScopedTypeVariables #-} ein, denn ich hasse es mich zu fragen, was forall an einem bestimmten Ort bedeutet. Ihre V Definition bedeutet genau das gleiche wie

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

können wir tatsächlich die explizite forall fallen, wenn wir mögen:

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

So ist die V Daten Konstruktor ist eine Funktion, die etwas von nimmt jede sendefähiges Typ und produziert etwas vom Typ V. Die Art der map ist ziemlich restriktiv:

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

Alle Elemente der Liste übergeben map den gleichen Typ haben müssen. So ist die Art von map V ist nur

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

Lassen Sie uns jetzt auf Ihren ersten Ausdruck zurück:

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

Nun, was das sagt eigentlich, dass [1, "a"] eine Liste ist, die jeweils deren Elemente hat forall a . Show a => a geben. Das heißt, wenn ich eine a, die eine Instanz von Show ist, bereitstellen, sollte jedes Element der Liste diesen Typ haben. Das ist einfach nicht wahr. "a" hat zum Beispiel nicht den Typ Bool. Es gibt noch ein anderes Problem hier; der Typ [forall a . Show a => a] ist "impredicative". Ich verstehe nicht die Details, was das bedeutet, aber locker gesagt haben Sie eine forall in das Argument eines anderen Typ Konstruktor als -> stecken, und das ist nicht erlaubt. GHC könnte vorschlagen, dass Sie die ImpredicativeTypes Erweiterung aktivieren, aber das funktioniert wirklich nicht richtig, also sollten Sie nicht. Wenn Sie eine Liste von existenziell quantifizierten Dingen haben möchten, müssen Sie sie zuerst in existenzielle Datentypen einbinden oder einen speziellen existenziellen Listentyp verwenden. Wenn Sie eine Liste von allgemein quantifizierten Dingen haben wollen, müssen Sie sie zuerst einpacken (wahrscheinlich in neuen Typen).