GADT dla polimorficznych listy

Question

ja parsowania kilka wypowiedzi postaci

v1 = expression1 
v2 = expression2 
... 

Używam State monady i mój stan powinien być parą (String, Expr a), naprawdę nalegać na posiadające wyrażenia wpisane. Starałem się wdrożyć państwo jako [PPair] gdzie mogę zdefiniować PPair przez GADT:

data PPair where 
    PPair :: (String, Expr a) -> PPair 

Gdy ta linia przeszła kompilator, czułem, że robię coś naprawdę bardzo złego. Stłumiłem tę myśl i kontynuowałem kodowanie. Kiedy przyjechałem do pisania kodu, które wyodrębnić wartość zmiennej od państwa, zdałem sobie sprawę z problemu:

evalVar k ((PPair (kk, v)):s) = if k == kk then v else evalVar k s 

uzyskać:

Inferred type is less polymorphic than expected 

który jest bardzo oczekiwane. Jak obejść ten problem? Wiem, że potrafię to rozwiązać, dzieląc typ na wszystkie typy kandydatów a, ale czy nie ma na to lepszego sposobu?

Answer 1

Problem polega na tym, że nie ma możliwości typ evalVar może mieć:

evalVar :: String -> [PPair] -> Expr ? 

Nie można powiedzieć ? jest a, bo wtedy jesteś twierdząc swoją wartość zwracana pracuje dowolny wartość a. Co można zrobić, jest jednak zakończyć "An Expr z nieznanego typu" do własnego typu danych:

data SomeExpr where 
    SomeExpr :: Expr a -> SomeExpr 

lub równoważnie z RankNTypes zamiast GADTs:

data SomeExpr = forall a. SomeExpr (Expr a) 

Jest nazwana egzystencjalna kwantyfikacja. Następnie można przepisać PPair użyciu SomeExpr:

data PPair = PPair String SomeExpr 

i evalVar odrabia: (. Oczywiście, można po prostu użyć [(String,SomeExpr)] zamiast, a standard lookup funkcję)

evalVar k (PPair kk v : xs) 
    | k == kk = v 
    | otherwise = evalVar k xs 

Ogólnie rzecz biorąc, próba zachowania wyrażeń całkowicie wpisanych na poziomie Haskella w ten sposób jest prawdopodobnie ćwiczeniem daremności; język zależny, taki jak Agda, nie miałby z tym problemu, ale prawdopodobnie skończy się na tym, że Haskell nie może zrobić dość szybko, lub osłabiając rzeczy do punktu, w którym bezpieczeństwo kompilacji wymagało wysiłku zgubiony.

To nie znaczy, że nigdy nie działa, oczywiście; języki pisane były jednym z motywujących przykładów GADT. Ale może nie działać tak dobrze, jak chcesz, i prawdopodobnie wpadniesz w kłopoty, jeśli twój język ma jakieś nietrywialne funkcje systemu typu, takie jak polimorfizm.

Jeśli naprawdę chcesz zachować pisanie, to użyłbym bogatszej struktury niż łańcuchy do nazwania zmiennych; mają Var a typ jawnie nosi typ, tak:

data PPair where 
    PPair :: Var a -> Expr a -> PPair 

evalVar :: Var a -> [PPair] -> Maybe (Expr a) 

Dobrym sposobem, aby osiągnąć coś podobnego do tego byłoby użyć pakietu vault; możesz zbudować Key s z ST i IO i użyć Vault jako heterogenicznego kontenera. Jest to zasadniczo jak Map, gdzie klucze zawierają typ odpowiadającej wartości. W szczególności zalecam zdefiniowanie Var a jako Key (Expr a) i użycie Vault zamiast Twojego [PPair]. (Pełne ujawnienie: Pracowałam na opakowaniu skarbca.)

Oczywiście, nadal będziesz mieć do odwzorowania nazw zmiennych z wartościami Key, ale można utworzyć wszystkie Key prawda po parsowania i wykonać ludzie wokół zamiast strun. (Z tą strategią byłoby trochę pracy od nazwy Var do odpowiadającej jej nazwy zmiennej; można to zrobić z listą elementów egzystencjalnych, ale rozwiązanie jest zbyt długie, aby wstawić tę odpowiedź.)

(Nawiasem mówiąc, możesz mieć wiele argumentów do konstruktora danych z GADT, tak jak zwykłe typy: data PPair where PPair :: String -> Expr a -> PPair.)