[Haskell-cafe] Can anybody give me some advice on this?

[Ryan Ingram]

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 <ryani.spam at gmail.com> 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 <6c5l7n at 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>