jak analizować łańcuchy do drzewa składni za pomocą GADTs

Question

Czytałem GADT wprowadzenie here i znalazłem pomysł ograniczenia programisty do tworzenia tylko odpowiedniego typu drzewa składni świetne, i umieściłem ten pomysł w moim prostym interpretatorze rachunku lambda, ale później zdałem sobie sprawę, że nie mogę parsować ciągu znaków do tego drzewa składni, ponieważ jedna funkcja parsowania musi zwracać różne typy drzew składniowych, w zależności od danych wejściowych. Oto przykład:

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

Przed użyciem GADTs używałem to:

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

GADTs są wielką przewagę tutaj, bacuse teraz nie mogę utworzyć nieprawidłowe drzew składniowych jak Lambda (Application ..) ...

Ale z GADTs, nie mogłem parsować ciąg i utworzyć drzewo parse. Oto parser dla Lambda, ozn i wyrażeń Zastosowanie:

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

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

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

Teraz problem jest:

expr = choice [ident, application, lambda] 

To oczywiście nie zadziała, ponieważ każdy parser wraca różnych typów.

Czy istnieje sposób na przeanalizowanie łańcucha znaków i utworzenie drzewa składni z GADT?

Answer 1

Możesz użyć GADT, aby utworzyć typ, który zawiera Expr a dla nieznanego a.

data AnyExpr where AnyExpr :: Expr a -> AnyExpr 

W sytuacjach, w których ty nie chcą ograniczyć Expr do konkretnego typu, należy AnyExpr.

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

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