
Hello, I am developing a very simple programming language for didactic purposes. Expressions can be composed of different types, like Int, Bool, String etc... The AST is compiled to JavaScript and the result is shown in the browser. The code is more or less like this: {-# LANGUAGE GADTs #-} data Expr a where Int :: Int -> Expr Int Bool :: Bool -> Expr Bool Text :: String -> Expr String -- Int operations Add :: Expr Int -> Expr Int -> Expr Int -- Bool operations And :: Expr Bool -> Expr Bool -> Expr Bool -- etc. etc. -- converts to JavaScript compile :: Expr a -> String compile (Int n) = show n compile (Text t) = show t compile (Add x y) = compile x ++ "+" ++ compile y -- etc. etc. The compilation works perfectly, but I am stuck with the parser. Since I don't know the types in advance, I would like to parse the whole expression at once. If I do: exprParser :: Parsec String u (Expr a) exprParser = parens exprParser <|> (reserved "true" >> return (Bool True)) <|> (reserved "false" >> return (Bool False)) <|> (stringLiteral >>= return . Text) The compiler says: "Couldn't match type `Bool' with `[Char]'" Where am I wrong?

On Sat, Feb 8, 2014 at 2:10 PM, Lorenzo Tabacchini
If I do:
exprParser :: Parsec String u (Expr a) exprParser = parens exprParser <|> (reserved "true" >> return (Bool True)) <|> (reserved "false" >> return (Bool False)) <|> (stringLiteral >>= return . Text)
The compiler says: "Couldn't match type `Bool' with `[Char]'" Where am I wrong?
The type of exprParser doesn't do what you intend. Specifically, the `a` in `(Expr a)` is chosen by the *caller* and you have to deal with that choice somehow --- it does not mean you can pick a different `a` in different parts of your code. There are several ways you might redesign your types, but I think I'll have to let someone else address those. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

On Sat, Feb 08, 2014 at 08:10:18PM +0100, Lorenzo Tabacchini wrote:
exprParser :: Parsec String u (Expr a) exprParser = parens exprParser <|> (reserved "true" >> return (Bool True)) <|> (reserved "false" >> return (Bool False)) <|> (stringLiteral >>= return . Text)
As Brandon explained, this type does not mean what you want: it promises to be able to return *any* type of Expr, but then it goes and tries to return *particular* types of Exprs. Of course, the type is a lie: you will only be able to return specific types of Exprs, but you can't know which ones in advance. In my opinion, this is one of the few places where existential wrappers are really what you want. If I were you, I would do something like this: data ExprE where ExprE :: Expr a -> ExprE -- existentially hides the expression type Now you can write your parser to return an ExprE, with the type of the expression hidden inside. In order to be able to use the resulting ExprE values, you will also want a function like withExprE :: ExprE -> (Expr a -> r) -> r withExprE (ExprE expr) k = k expr -Brent

In my opinion, this is one of the few places where existential wrappers are really what you want. If I were you, I would do something like this:
data ExprE where ExprE :: Expr a -> ExprE -- existentially hides the expression type
Now you can write your parser to return an ExprE, with the type of the expression hidden inside. In order to be able to use the resulting ExprE values, you will also want a function like
withExprE :: ExprE -> (Expr a -> r) -> r withExprE (ExprE expr) k = k expr
Thanks. This is the kind of solution I was looking for. The problem is, when I try to access the "hidden" Expr type the compiler complains: Couldn't match type `a1' with `a' `a1' is a rigid type variable bound by a pattern with constructor ExprE :: forall a. Expr a -> ExprE, in an equation for `withExprE' `a' is a rigid type variable bound by the type signature for withExprE :: ExprE -> (Expr a -> r) -> r

On Sun, Feb 09, 2014 at 09:21:15AM +0100, Lorenzo wrote:
In my opinion, this is one of the few places where existential wrappers are really what you want. If I were you, I would do something like this:
data ExprE where ExprE :: Expr a -> ExprE -- existentially hides the expression type
Now you can write your parser to return an ExprE, with the type of the expression hidden inside. In order to be able to use the resulting ExprE values, you will also want a function like
withExprE :: ExprE -> (Expr a -> r) -> r withExprE (ExprE expr) k = k expr
Thanks. This is the kind of solution I was looking for. The problem is, when I try to access the "hidden" Expr type the compiler complains:
Whoops! Sorry, I gave you the wrong type for withExprE. And you can see why it is wrong, based on the earlier explanation: the *caller* of withExprE gets to choose the type a, but there is some particular (unknown) type inside the ExprE, so there is no guarantee they will match up. Instead, we must write withExprE :: ExprE -> (forall a. Expr a -> r) -> r (note you have to enable the Rank2Types extension). This says that the caller of ExprE must provide a function which works *no matter what* the type a is, i.e. the implementation of withExprE gets to choose the type a, rather than the caller. -Brent
participants (4)
-
Brandon Allbery
-
Brent Yorgey
-
Lorenzo
-
Lorenzo Tabacchini