come analizzare le stringhe per la sintassi dell'albero utilizzando GADT

Question

Stavo leggendo GADT introduzione here e ho trovato l'idea di limitare il programmatore per creare solo il giusto tipo di albero di sintassi ottimo, e ho inserito questa idea nel mio semplice interprete di calcolo lambda, ma più tardi mi sono reso conto che non posso analizzare una stringa su questo albero di sintassi, perché una funzione di analisi deve restituire diversi tipi di albero di sintassi, a seconda dell'input. Ecco un esempio:

{-# LANGUAGE GADTs #-} 
data Ident 
data Lambda 
data Application 

data Expr a where 
    Ident :: String -> Expr Ident 
    Lambda :: Expr Ident -> Expr a -> Expr Lambda 
    Application :: Expr a -> Expr a -> Expr Application 

Prima di utilizzare GADTs, stavo usando questo:

data Expr = Lambda Expr Expr 
      | Ident String 
      | Application Expr Expr 

GADTs sono grande vantaggio qui, bacuse ora non posso creare alberi di sintassi non validi come Lambda (Application ..) ...

Ma con GADT, non è stato possibile analizzare una stringa e creare un albero di analisi. Qui ci sono parser per Lambda, Ident, e le espressioni di applicazione:

ident :: Parser (Expr Ident) 
ident = ... 

lambda :: Parser (Expr Lambda) 
lambda = ... 

application :: Parser (Expr Application) 
application = ... 

Ora il problema è:

expr = choice [ident, application, lambda] 

Questo, ovviamente, non funziona, dal momento che ogni parser sta tornando tipi diversi.

Quindi, c'è un modo per analizzare una stringa e creare un albero di sintassi, con GADT?

Answer 1

È possibile utilizzare GADT per creare un tipo che contiene Expr a per alcuni sconosciuti a.

data AnyExpr where AnyExpr :: Expr a -> AnyExpr 

In situazioni in cui non si vogliono limitare Expr a un tipo specifico, utilizzare AnyExpr.

anyExpr :: Parser (Expr a) -> Parser AnyExpr 
anyExpr p = fmap AnyExpr p 

expr :: Parser AnyExpr 
expr = choice [anyExpr ident, anyExpr application, anyExpr lambda]