Dlaczego `[1," a "] :: [forall a. Pokaż a => a] `jest niedozwolone?

Question

W moim (może być niepoprawne) zrozumienia po obu listach powinny być równoważne:

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

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

Jednak pierwsze nie jest akceptowane, ale druga działa prawidłowo (z ExistentialQuantification).

Jeśli pierwsza lista nie istnieje, jaki byłby typ w pustym polu map V :: ??? -> [V]? Jaki mechanizm typu wymusza istnienie opakowania?

Answer 1

Twoje zrozumienie jest nieprawidłowe. Duża część problemu polega na tym, że tradycyjna składnia ilościowa, którą stosowałeś, jest dość myląca dla każdego, kto nie jest do niej dobrze zaznajomiony. Dlatego zdecydowanie zalecam stosowanie składni GADT, która ma również zaletę, że jest ściśle silniejsza. Prostą czynnością jest włączenie {-# LANGUAGE GADTs #-}. Kiedy już jesteśmy, włączmy {-# LANGUAGE ScopedTypeVariables #-}, ponieważ nie znoszę zastanawiać się, co oznacza forall w danym miejscu. Twój V definicja oznacza dokładnie to samo, co

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

Możemy faktycznie spadek wyraźnej forall jeśli lubimy:

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

Więc konstruktor dane V to funkcja, która bierze coś dowolny showable wpisz i produkuje coś typu V. Rodzaj map jest dość restrykcyjna:

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

Wszystkie elementy listy przekazywane do map mieć ten sam typ. Tak typ map V tylko

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

Wróćmy do pierwszego wyrazu teraz:

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

Teraz co to faktycznie mówi, że [1, "a"] jest lista, każdy z którego elementy ma typ forall a . Show a => a. Oznacza to, że jeśli dostarczę dowolną wersję a, która jest instancją Show, każdy element listy powinien mieć ten typ. To po prostu nieprawda. "a" nie ma na przykład typu Bool. Jest jeszcze inny problem; typ [forall a . Show a => a] jest "nieprzewidywalny". Nie rozumiem szczegółów tego, co to oznacza, ale luźno mówiąc utknąłeś w argumencie konstruktora typu innego niż ->, a to nie jest dozwolone. GHC może sugerować włączenie rozszerzenia ImpredicativeTypes, ale to naprawdę nie działa poprawnie, więc nie powinieneś. Jeśli chcesz mieć listę rzeczy, które istnieją ilościowo, musisz zawinąć je najpierw w egzystencjalne typy danych lub użyć wyspecjalizowanego typu list egzystencjalnych. Jeśli chcesz mieć listę rzeczy o uniwersalnych liczbach, musisz najpierw je zawinąć (prawdopodobnie w newtypach).