8

我在这里阅读 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 解析字符串并创建语法树？

4

1 回答 1

8

您可以使用 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]
于 2012-06-19T15:45:35.760 回答