如何使用GADT将字符串解析为语法树

Question

我正在阅读这里的 GADT介绍,我发现限制程序员创建只有正确类型的语法树很好的想法,我把这个想法放到我的简单lambda演算解释器中,但后来我意识到我无法解析字符串到这个语法树,因为一个解析函数需要返回不同类型的语法树,具体取决于输入.这是一个例子:

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

在使用GADT之前,我使用的是:

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

GADT在这里很有优势,现在我无法创建无效的语法树Lambda (Application ..) ...

但是使用GADT,我无法解析字符串并创建解析树.以下是Lambda,Ident和Application表达式的解析器:

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

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

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

现在的问题是:

expr = choice [ident, application, lambda]

这显然不起作用,因为每个解析器返回不同的类型.

那么,有没有办法解析字符串并使用GADT创建语法树？

Answer 1

您可以使用GADT创建包含Expr a某些未知类型的类型a.

data AnyExpr where AnyExpr :: Expr a -> AnyExpr

在你的情况不希望限制Expr到特定的类型,使用AnyExpr.

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

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