Can anybody give me some advice on this?
Hello everybody, I have a piece of code that gives me headaches for some time now. Simply put, I would like to know which is the best way to overpass a "Couldn't match expected type * against inferred type *"-error and an "Occurs check: cannot construct the infinite type:"-error in the following situation: {-# OPTIONS -fglasgow-exts #-}
module Simple where import Text.ParserCombinators.Parsec
data HData a = O | C a deriving (Eq,Ord,Show) data IN l = IN Int (HData l) deriving (Eq,Ord,Show) data CH l = CH Char (HData l) deriving (Eq,Ord,Show) -- data type is well-defined: sample = C(IN 0 (C(CH 'a' (C(IN 1 (C(CH 'b' (C(IN 2 O)))))))))
embeddedParser types = do string "end"; spaces; return O {- <|> do let h = head types let t = tail types case h of 1 -> do aux <- pInt rest <- embeddedParser $t++[h] return $ C (IN aux rest) 2 -> do aux <- pCh rest <- embeddedParser $t++[h] return $ C (CH aux rest) _ -> error "unallowed type" -} pInt = do n <- fmap read $ many1 digit; return $ fromInteger n pCh = do c <- letter; return $ c simple = embeddedParser [1,2]
-- the above result from sample I would like to get by running -- parseTest simple "0a1b2end"
The way I see it, the defined datatype works but I am a bit clueless about how to modify the parser to accept things of the type (e.g.): HData (IN (CH (IN (CH (IN a))))) (and in general of any finite type embedded like this). Thanks in advance for your help, George
The problem is this: what is the type of "embeddedParser"? Unless you can answer that question, you're not going to be able to write it. In particular, its *type* depends on the *value* of its argument; the type of embeddedParser [1,2] is different from the type of embeddedParser [1,1,2]. This isn't possible in Haskell; you need a language with an even more exotic type system (Agda, for example) to encode this dependency. Google "dependent types" for more information. You can encode something similar using existentials: data Sealed p = forall a. Sealed (p a) type ParseResult = Sealed HData ... case h of 1 -> do aux <- pInt Sealed rest <- embeddedParser (t ++ [h]) return (Sealed (C (In aux rest))) and a similar transformation on the (2) case and the "end" case; this makes the type of embeddedParser into Parser ParseResult. What you are doing here is saying that the result of a parse is an HData a for *some* a, but you aren't saying which one. You extract the HData from the existential when running the sub parser, then stuff it back into another existential. But you can't extract the type out of the existential ever; it is lost. In particular you can't prove to the compiler that the type matches that of the [1,2] input and get back to the IN and CH values. And you can't return a value that has been extracted out, you can only stuff it back into another existential container or consume it in some other way! A better option is to use a type that matches what you expect to parse, or just use Data.Dynamic if you want multiple types. You aren't going to get any benefit from "HData a" without a lot more type-level work! Also, for your type list, it'd be much more efficient to use (cycle types) to construct an infinite list (in finite space!) rather than keep appending the head back onto the tail. 2008/12/1 Georgel Calin <6c5l7n@googlemail.com>:
Hello everybody,
I have a piece of code that gives me headaches for some time now.
Simply put, I would like to know which is the best way to overpass a "Couldn't match expected type * against inferred type *"-error and an "Occurs check: cannot construct the infinite type:"-error in the following situation:
{-# OPTIONS -fglasgow-exts #-} module Simple where import Text.ParserCombinators.Parsec
data HData a = O | C a deriving (Eq,Ord,Show) data IN l = IN Int (HData l) deriving (Eq,Ord,Show) data CH l = CH Char (HData l) deriving (Eq,Ord,Show) -- data type is well-defined: sample = C(IN 0 (C(CH 'a' (C(IN 1 (C(CH 'b' (C(IN 2 O)))))))))
embeddedParser types = do string "end"; spaces; return O {- <|> do let h = head types let t = tail types case h of 1 -> do aux <- pInt rest <- embeddedParser $t++[h] return $ C (IN aux rest) 2 -> do aux <- pCh rest <- embeddedParser $t++[h] return $ C (CH aux rest) _ -> error "unallowed type" -} pInt = do n <- fmap read $ many1 digit; return $ fromInteger n pCh = do c <- letter; return $ c simple = embeddedParser [1,2]
-- the above result from sample I would like to get by running -- parseTest simple "0a1b2end"
The way I see it, the defined datatype works but I am a bit clueless about how to modify the parser to accept things of the type (e.g.): HData (IN (CH (IN (CH (IN a))))) (and in general of any finite type embedded like this).
Thanks in advance for your help, George _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Also, if you can give up on the dependent types issue, and you just want the equivalent of "embeddedParser [1,2]", you have a problem that the type you are specifying is infinite; this is the cause of the "occurs checks" errors you are getting. Lets specify the type you are parsing directly, then abstract a bit:
-- your HData is just Maybe!
data IN1 = IN1 Int (Maybe CH1) data CH1 = CH1 Char (Maybe IN1)
sample :: Maybe IN1 sample = Just $ IN1 0 $ Just $ CH1 'a' $ Just $ IN1 1 $ Just $ CH1 'b' $ Just $ IN1 2 $ Nothing
You can easily write a parser for this type with two mutually recursive parsers that parse IN1 and CH1; I'll leave that as an exercise for you. Now, you might not want to explicitly specify the type of the result in the data type; that's what you have done with your versions of IN and CH that take the "rest of the type" as an argument. But the problem with that approach is that the resultant type is *infinite*!
data -- broken: -- type ParserResult = Maybe (IN (Maybe (CH (Maybe (IN (Maybe ...
But there is a great trick to solve this; another type can wrap the "fixpoint" of this type:
newtype Mu f = In (f (Mu f)) out (In x) = x
You can then use this structure to define the type of the parser:
data ResultOpen a = O | C (IN (ResultOpen (CH (ResultOpen a)))) type Result = Mu ResultOpen
What "Mu" does here is fill in the "a" in ResultOpen with (ResultOpen (ResultOpen (ResultOpen (ResultOpen ..., infinitely large. The price you pay for this infinite type is that you have to explicitly mark the boundaries with "In"; the constructor for "Mu":
sample2 :: Result sample2 = In (C(IN 0 (C(CH 'a' (In (C(IN 1 (C(CH 'b' (In (C(IN 2 O))))))))))))
A parser for this type is also not too difficult to write; you just
have to take care to use "In" and "out" in the right places.
-- ryan
On Mon, Dec 1, 2008 at 6:08 PM, Ryan Ingram
The problem is this: what is the type of "embeddedParser"? Unless you can answer that question, you're not going to be able to write it.
In particular, its *type* depends on the *value* of its argument; the type of embeddedParser [1,2] is different from the type of embeddedParser [1,1,2]. This isn't possible in Haskell; you need a language with an even more exotic type system (Agda, for example) to encode this dependency. Google "dependent types" for more information.
You can encode something similar using existentials:
data Sealed p = forall a. Sealed (p a) type ParseResult = Sealed HData
...
case h of 1 -> do aux <- pInt Sealed rest <- embeddedParser (t ++ [h]) return (Sealed (C (In aux rest)))
and a similar transformation on the (2) case and the "end" case; this makes the type of embeddedParser into Parser ParseResult. What you are doing here is saying that the result of a parse is an HData a for *some* a, but you aren't saying which one. You extract the HData from the existential when running the sub parser, then stuff it back into another existential.
But you can't extract the type out of the existential ever; it is lost. In particular you can't prove to the compiler that the type matches that of the [1,2] input and get back to the IN and CH values. And you can't return a value that has been extracted out, you can only stuff it back into another existential container or consume it in some other way!
A better option is to use a type that matches what you expect to parse, or just use Data.Dynamic if you want multiple types. You aren't going to get any benefit from "HData a" without a lot more type-level work!
Also, for your type list, it'd be much more efficient to use (cycle types) to construct an infinite list (in finite space!) rather than keep appending the head back onto the tail.
2008/12/1 Georgel Calin <6c5l7n@googlemail.com>:
Hello everybody,
I have a piece of code that gives me headaches for some time now.
Simply put, I would like to know which is the best way to overpass a "Couldn't match expected type * against inferred type *"-error and an "Occurs check: cannot construct the infinite type:"-error in the following situation:
{-# OPTIONS -fglasgow-exts #-} module Simple where import Text.ParserCombinators.Parsec
data HData a = O | C a deriving (Eq,Ord,Show) data IN l = IN Int (HData l) deriving (Eq,Ord,Show) data CH l = CH Char (HData l) deriving (Eq,Ord,Show) -- data type is well-defined: sample = C(IN 0 (C(CH 'a' (C(IN 1 (C(CH 'b' (C(IN 2 O)))))))))
embeddedParser types = do string "end"; spaces; return O {- <|> do let h = head types let t = tail types case h of 1 -> do aux <- pInt rest <- embeddedParser $t++[h] return $ C (IN aux rest) 2 -> do aux <- pCh rest <- embeddedParser $t++[h] return $ C (CH aux rest) _ -> error "unallowed type" -} pInt = do n <- fmap read $ many1 digit; return $ fromInteger n pCh = do c <- letter; return $ c simple = embeddedParser [1,2]
-- the above result from sample I would like to get by running -- parseTest simple "0a1b2end"
The way I see it, the defined datatype works but I am a bit clueless about how to modify the parser to accept things of the type (e.g.): HData (IN (CH (IN (CH (IN a))))) (and in general of any finite type embedded like this).
Thanks in advance for your help, George _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (2)
-
Georgel Calin -
Ryan Ingram