Arithmetic expressions with GADTs: parsing

Hello. In order to learn GADTs, I have written the attached program, which defines a type for arithmetic expressions using GADTs, a parser for them, and an evaluation function. But my parser does not typecheck. ghc-7.4.1 gives me the error message: Expr.hs:25:28: Couldn't match expected type `Double' with actual type `Bool' Expected type: Bool -> Expr Double Actual type: Bool -> Expr Bool In the first argument of `(<$>)', namely `B' In the first argument of `(<|>)', namely `B <$> pBool' Any clues on how to fix that? Romildo

* j.romildo@gmail.com
Hello.
In order to learn GADTs, I have written the attached program, which defines a type for arithmetic expressions using GADTs, a parser for them, and an evaluation function.
But my parser does not typecheck. ghc-7.4.1 gives me the error message:
Expr.hs:25:28: Couldn't match expected type `Double' with actual type `Bool' Expected type: Bool -> Expr Double Actual type: Bool -> Expr Bool In the first argument of `(<$>)', namely `B' In the first argument of `(<|>)', namely `B <$> pBool'
Any clues on how to fix that?
The alternatives given to <|> must be of the same type. In your case, one is Expr Double and one is Expr Bool. Inclusion of pBool in pFactor is probably a mistake — unless you're going to multiply booleans. -- Roman I. Cheplyaka :: http://ro-che.info/

On Wed, May 02, 2012 at 03:02:46PM +0300, Roman Cheplyaka wrote:
* j.romildo@gmail.com
[2012-05-02 08:03:45-0300] [...] The alternatives given to <|> must be of the same type. In your case, one is Expr Double and one is Expr Bool. Inclusion of pBool in pFactor is probably a mistake — unless you're going to multiply booleans.
You are right in the sense that I cannot mix Expr Bool and Expr Double in a (O op l r) expression. But the parser should be able to parse any form of expressions. So I rewrite my program to take this into account. The new versions still does not compile: Expr.hs:27:23: Couldn't match expected type `Double' with actual type `Bool' Expected type: ParsecT String () Data.Functor.Identity.Identity (Expr Double) Actual type: ParsecT String () Data.Functor.Identity.Identity (Expr Bool) In the first argument of `(<|>)', namely `pBool' In the second argument of `(<|>)', namely `pBool <|> pEqual' Romildo

Hi Romildo, On Wed, May 2, 2012 at 3:08 PM, j.romildo wrote:
You are right in the sense that I cannot mix Expr Bool and Expr Double in a (O op l r) expression.
But the parser should be able to parse any form of expressions. So I rewrite my program to take this into account.
The new versions still does not compile:
Expr.hs:27:23: Couldn't match expected type `Double' with actual type `Bool' Expected type: ParsecT String () Data.Functor.Identity.Identity (Expr Double) Actual type: ParsecT String () Data.Functor.Identity.Identity (Expr Bool) In the first argument of `(<|>)', namely `pBool' In the second argument of `(<|>)', namely `pBool <|> pEqual'
From this, we see that the same type parameters to ParsecT are used in the two argument types as well as the result type. We also see that (<|>) is a right-associative infix operator. So, this means the offending line could be parenthesized as pArit <|> (pBool <|> pEqual), which fits the second
You appear to still be having the same problem. Perhaps this because you don't quite understand the type error? Let me help you dissect it. Since this is a type error, I'm not going to assume anything about what should or should not work. I'll only look at the types. First, let's comment out the offending line, so that your file type-checks: Line 27: -- pExpr = pArit <|> pBool <|> pEqual Next, let's look at each of the components relevant to the type error. The first mentioned is (<|>). In GHCi, we can find out more information about that: *Expr> :i (<|>) (<|>) :: ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a -- Defined in Text.Parsec.Prim infixr 1 <|> part of the type error, pBool <|> pEqual. Looking at the types of those, we see: *Expr> :t pBool pBool :: ParsecT String () Data.Functor.Identity.Identity (Expr Bool) *Expr> :t pEqual pEqual :: ParsecT String () Data.Functor.Identity.Identity (Expr Double) As we saw with the type of (<|>), these two types should be the "same" (as in unifiable). However, they are not, because the two type arguments to the Expr GADT differ: Bool in one case and Double in the other. GHC cannot "match" (unify) these types. Now, to the goal of your project: You say that the parser "should be able to parse any form of expressions," but since you are using a GADT with the expected expression types in the result index of each constructor, you can only define parsers that each parse an expression of a single type. That is, you can have a parser for Expr Bool and a parser for Expr Double, but these parsers can not be alternatives of another Expr and still have a valid type. This is, of course, the reason for using the type index as it is: you don't want Bool where you expect Double and vice versa. As a general comment, you may want to consider simplifying your goal to parsing only expressions of type Double. Then, what happens to your Bool constructors? Well, you could drop them, or you could extend your GADT with an "if" constructor that takes a boolean condition with Double alternatives. Regards, Sean

Another option is to reify the type so that you can get it back somehow.
Here's a few diffs to your file (I've attached the full code):
A new type:
data Typed f where
TDouble :: f Double -> Typed f
TBool :: f Bool -> Typed f
runT :: (f Double -> a) -> (f Bool -> a) -> Typed f -> a
runT k _ (TDouble x) = k x
runT _ k (TBool x) = k x
New version of pExpr that can parse both expression types, by tagging with
the type
-- pExpr = pArit <|> pBool <|> pEqual
pExpr = (TDouble <$> pArit) <|> (TBool <$> pBool) <|> (TDouble <$>
pEqual)
and now main:
main = do line <- getLine
case parse pExpr "" line of
Left msg -> putStrLn (show msg)
Right e -> putStrLn (runT (show . eval) (show . eval) e)
What I'm doing here is reifying the possible types of top level expressions
and then providing a handler in main which works on all possible types.
There are other ways to do this (embed any expression in an existential,
for example), but this makes it really clear what is going on, and shows
the way forward for parsing a larger typed language.
-- ryan
On Wed, May 2, 2012 at 6:08 AM,
On Wed, May 02, 2012 at 03:02:46PM +0300, Roman Cheplyaka wrote:
* j.romildo@gmail.com
[2012-05-02 08:03:45-0300] [...] The alternatives given to <|> must be of the same type. In your case, one is Expr Double and one is Expr Bool. Inclusion of pBool in pFactor is probably a mistake — unless you're going to multiply booleans.
You are right in the sense that I cannot mix Expr Bool and Expr Double in a (O op l r) expression.
But the parser should be able to parse any form of expressions. So I rewrite my program to take this into account.
The new versions still does not compile:
Expr.hs:27:23: Couldn't match expected type `Double' with actual type `Bool' Expected type: ParsecT String () Data.Functor.Identity.Identity (Expr Double) Actual type: ParsecT String () Data.Functor.Identity.Identity (Expr Bool) In the first argument of `(<|>)', namely `pBool' In the second argument of `(<|>)', namely `pBool <|> pEqual'
Romildo
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Very useful to get a gadt back to monotype without an existential, which
would mean to use classes for future uses of it with its load of object
oriented thinking.
Thanks for sharing.
paolino
2012/6/4 Ryan Ingram
Another option is to reify the type so that you can get it back somehow. Here's a few diffs to your file (I've attached the full code):
A new type: data Typed f where TDouble :: f Double -> Typed f TBool :: f Bool -> Typed f
runT :: (f Double -> a) -> (f Bool -> a) -> Typed f -> a runT k _ (TDouble x) = k x runT _ k (TBool x) = k x
New version of pExpr that can parse both expression types, by tagging with the type
-- pExpr = pArit <|> pBool <|> pEqual pExpr = (TDouble <$> pArit) <|> (TBool <$> pBool) <|> (TDouble <$> pEqual)
and now main: main = do line <- getLine case parse pExpr "" line of Left msg -> putStrLn (show msg) Right e -> putStrLn (runT (show . eval) (show . eval) e)
What I'm doing here is reifying the possible types of top level expressions and then providing a handler in main which works on all possible types. There are other ways to do this (embed any expression in an existential, for example), but this makes it really clear what is going on, and shows the way forward for parsing a larger typed language.
-- ryan
On Wed, May 2, 2012 at 6:08 AM,
wrote: On Wed, May 02, 2012 at 03:02:46PM +0300, Roman Cheplyaka wrote:
* j.romildo@gmail.com
[2012-05-02 08:03:45-0300] [...] The alternatives given to <|> must be of the same type. In your case, one is Expr Double and one is Expr Bool. Inclusion of pBool in pFactor is probably a mistake — unless you're going to multiply booleans.
You are right in the sense that I cannot mix Expr Bool and Expr Double in a (O op l r) expression.
But the parser should be able to parse any form of expressions. So I rewrite my program to take this into account.
The new versions still does not compile:
Expr.hs:27:23: Couldn't match expected type `Double' with actual type `Bool' Expected type: ParsecT String () Data.Functor.Identity.Identity (Expr Double) Actual type: ParsecT String () Data.Functor.Identity.Identity (Expr Bool) In the first argument of `(<|>)', namely `pBool' In the second argument of `(<|>)', namely `pBool <|> pEqual'
Romildo
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (5)
-
j.romildo@gmail.com
-
Paolino
-
Roman Cheplyaka
-
Ryan Ingram
-
Sean Leather