how to parse strings to syntax tree using GADTs

Question

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 ?

Heatsink Heatsink · Accepted Answer · 2012-06-19T15:45:35

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]

how to parse strings to syntax tree using GADTs

1 Answers