GADT per la lista polimorfico

Question

Io sono l'analisi di un paio di dichiarazioni del modulo

v1 = expression1 
v2 = expression2 
... 

Sto usando lo Stato Monade e il mio stato dovrebbe essere un paio di (String, Expr a), ho davvero insistere per avere la espressioni digitate. Ho cercato di implementare lo stato come [PPair] dove mi definisco PPair dal GADT:

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

Una volta che questa linea superato il compilatore, ho sentito che sto facendo qualcosa di veramente veramente sbagliato. Ho soppresso il pensiero e ho continuato a scrivere codice. Quando sono arrivato a scrivere il codice che estrarre il valore della variabile da parte dello Stato, mi sono reso conto del problema:

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

ottengo:

Inferred type is less polymorphic than expected 

che è molto atteso. Come posso risolvere questo problema? So che posso risolverlo rompendo il tipo su tutti i tipi di candidati a, ma non esiste un modo più ordinato?

Answer 1

Il problema è che non c'è nessun tipo possibile evalVar può avere:

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

Non si può dire ? è a, perché allora si sta rivendicando il tuo valore di ritorno funziona per qualsiasi valore a. Cosa si può fare, però, è avvolgere "un Expr con un tipo sconosciuto" in un proprio tipo di dati:

data SomeExpr where 
    SomeExpr :: Expr a -> SomeExpr 

o, equivalentemente, con RankNTypes piuttosto che GADTs:

data SomeExpr = forall a. SomeExpr (Expr a) 

Questo è chiamata quantificazione esistenziale. È quindi possibile riscrivere PPair usando SomeExpr:

data PPair = PPair String SomeExpr 

e evalVar risolve: (. Naturalmente, si potrebbe utilizzare un [(String,SomeExpr)] invece, e la funzione standard lookup)

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

In generale, tuttavia, provare a mantenere espressioni digitate completamente a livello di Haskell come questo è probabilmente un esercizio di futilità; un linguaggio tipizzato come Agda non avrebbe problemi con esso, ma probabilmente finirai per imbattersi in qualcosa che Haskell non può fare abbastanza rapidamente, o indebolire le cose fino al punto in cui la sicurezza in fase di compilazione volevi dallo sforzo è perduto.

Ciò non significa che non funzioni mai, naturalmente; le lingue tipizzate erano uno degli esempi motivanti per le GADT. Ma potrebbe non funzionare come vuoi, e probabilmente ti troverai nei guai se la tua lingua ha caratteristiche di sistema di tipo non banale come il polimorfismo.

Se si desidera mantenere la digitazione, utilizzare una struttura più ricca rispetto alle stringhe per denominare le variabili; avere un tipo di Var a che trasporta in modo esplicito il tipo, in questo modo:

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

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

Un buon modo per ottenere qualcosa di simile a questo sarebbe quella di utilizzare il pacchetto vault; è possibile costruire Key s da ST e IO e utilizzare Vault come contenitore eterogeneo. È fondamentalmente come un Map in cui le chiavi contengono il tipo del valore corrispondente. Nello specifico, suggerirei di definire Key (Expr a) come Key (Expr a) e di utilizzare uno Vault anziché il [PPair]. (Full disclosure: Ho lavorato sulla confezione volta.)

Naturalmente, avrai ancora per mappare i nomi delle variabili ai valori Key, ma è possibile creare tutte le Key s destra dopo l'analisi, e trasportare quelli intorno invece delle corde. (Sarebbe un po 'di lavoro andare da un Var al suo nome di variabile corrispondente con questa strategia, però, puoi farlo con un elenco di elementi esistenziali, ma la soluzione è troppo lunga per inserire questa risposta.)

(A proposito, puoi avere più argomenti per un costruttore di dati con GADT, proprio come i tipi regolari: data PPair where PPair :: String -> Expr a -> PPair.)