如何使用GADT将字符串解析到语法树(how to parse strings to syntax tree using GADTs)

如何使用GADT将字符串解析到语法树(how to parse strings to syntax tree using GADTs)

我在这里阅读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创建一个语法树？

I was reading GADT introduction here and it I found the idea of restricting programmer to create only right type of syntax tree great, and I put this idea into my simple lambda calculus interpreter, but later I realized that I can't parse a string to this syntax tree, because one parse function needs to return different types of syntax tree, depending on input. Here's an example:

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

Before using GADTs, I was using this:

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

GADTs are great advantage here, bacuse now I can't create invalid syntax trees like Lambda (Application ..) ...

But with GADTs, I couldn't parse a string and create parse tree. Here are parser for Lambda, Ident, and Application expressions:

ident :: Parser (Expr Ident) ident = ... lambda :: Parser (Expr Lambda) lambda = ... application :: Parser (Expr Application) application = ...

Now the problem is:

expr = choice [ident, application, lambda]

This obviously doesn't work, since each parser is returning different types.

So, is there a way to parse a string and create a syntax tree, with GADTs ?

最满意答案

您可以使用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]

You can use GADTs to make a type that contains Expr a for some unknown a.

data AnyExpr where AnyExpr :: Expr a -> AnyExpr

In situations where you don't want to restrict Expr to a specific type, use AnyExpr.

anyExpr :: Parser (Expr a) -> Parser AnyExpr anyExpr p = fmap AnyExpr p expr :: Parser AnyExpr expr = choice [anyExpr ident, anyExpr application, anyExpr lambda]