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 [EMAIL PROTECTED] wrote:
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 [EMAIL PROTECTED]:
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
