wie man Zeichenketten zum Syntaxbaum mit GADTs analysieren

Question

Ich las GADT Einleitung here und es fand ich die Idee des Beschränkens des Programmierers, um nur richtigen Typ des Syntaxbaums groß zu schaffen, und ich legte diese Idee in meinen einfachen Lambda-Kalkülinterpreter, aber später wurde mir klar, dass ich eine Zeichenkette nicht in diesen Syntaxbaum einlesen kann, da eine Parse-Funktion abhängig von der Eingabe verschiedene Arten von Syntaxbäumen zurückgeben muss. Hier ein Beispiel:

{-# 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 

Vor GADTs verwendet, war ich mit dieser:

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

GADTs sind großer Vorteil hier, bacuse jetzt kann ich nicht ungültig Syntaxbäume erstellen wie Lambda (Application ..) ...

Aber mit GADTs konnte ich eine Zeichenfolge nicht analysieren und Parse-Struktur erstellen. Hier sind Parser für Lambda, Ident und Anwendungs ​​Ausdrücke:

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

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

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

Das Problem ist jetzt:

expr = choice [ident, application, lambda] 

Das ist offensichtlich nicht funktioniert, da jeder Parser verschiedene Arten zurückkehrt.

Gibt es also eine Möglichkeit, eine Zeichenfolge zu analysieren und einen Syntaxbaum mit GADTs zu erstellen?

Answer 1

Sie können GADTs verwenden, um einen Typ zu erstellen, der Expr a für einige unbekannte a enthält.

data AnyExpr where AnyExpr :: Expr a -> AnyExpr 

In Situationen, in denen Sie nicht wollen tun Expr auf eine bestimmte Art zu beschränken, AnyExpr verwenden.

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

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