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

Question

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

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