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

我正在阅读GADT介绍here，它发现限制程序员只创建正确类型的语法树的想法很好，我把这个想法放入我的简单lambda演算解释器中，但后来我意识到我无法解析字符串到这个语法树，因为一个解析函数需要根据输入返回不同类型的语法树。这里有一个例子：如何使用GADT解析字符串到语法树

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

使用GADTs之前，我用的是这样的：

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

GADTs这里有很大的优势，bacuse现在我无法创建无效语法树像Lambda (Application ..) ..。

但是对于GADT，我无法解析字符串并创建解析树。下面是LAMBDA，订货号和应用表达式解析器：

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

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

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

现在的问题是：

expr = choice [ident, application, lambda]

这显然是行不通的，因为每个解析器将返回不同的类型。

那么，有没有办法解析一个字符串，并创建一个语法树，与GADTs？

来源

2012-06-19 sinan

对于某些未知的a，您可以使用GADT制作一个包含Expr 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]

来源

2012-06-19 15:45:35 Heatsink

这是一个好主意，谢谢！但我仍然怀疑我们是否有其他方法来做我想做的事情，以及我所做的是否是一个好主意。 – sinan

@sinan - 这很好，但另一种方法是定义两个AST，一个用于解析输出，另一个用于实际使用。解析输出树将是无类型的，工作AST将使用GADT，就像您已经实现的一样。 –

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

回答

相关问题