[Haskell-cafe] Parsec and type level numerals

[Ryan Ingram]

You're almost there, but you have correctly determined the problem;
you need to know the type of the parse result in order to parse.

However, it is possible to hide the type from the parser; try writing
this function instead:

{-# LANGUAGE ExistentialQuantification #-}
data AnyCard = forall t. Card t => AnyCard t

parseP :: Parser AnyCard

Now the type-level numeral is hidden in the "AnyCard" existential
type.  In order to use it, you need to be able to use operations that
work on any instance of Card, which means the class/instance
declarations you have so far aren't that useful.  Emulating dependent
types using existentials in Haskell is never pretty!

Another option is to use a GADT to hold the type:

{-# LANGUAGE GADTs, ExistentialQuantification #-}

data GADTNum t where
    GZero :: GADTNum Zero
    GSucc :: GADTNum a -> GADTNum (Succ a)
data AnyCard = forall t. AnyCard (GADTNum t)

Now, after the parse, you can use the structure of the GADT to
determine things about the existential type:

isTwo :: AnyCard -> Maybe (Succ (Succ Zero))
isTwo (AnyCard (GSucc (GSucc GZero))) = Succ (Succ Zero)
isTwo _ = Nothing

  -- ryan

2008/12/13 Nathan Bloomfield <nbloomf at gmail.com>:
> Hello all. I've got a puzzling Parsec problem. Perhaps the collective wisdom
> of haskell-cafe can point me in the right direction.
>
> I want to be able to parse a string of digits to a type level numeral as
> described in the Number parameterized types paper. After fiddling with the
> problem for a while, I'm not convinced it's possible- it seems as though one
> would need to know the type of the result before parsing, but then we
> wouldn't need to parse in the first place. :) My first (simplified)
> approximation is as follows:
>
>> data Zero = Zero
>> data Succ a = Succ a
>
>> class Card t
>> instance Card Zero
>> instance (Card a) => Card (Succ a)
>
>> parseP :: (Card a) => Parser a
>> parseP = do { char '1'
>>             ; rest <- parseP
>>             ; return $ Succ rest
>>             }
>>          <|> return Zero
>
> I'd like for this to parse, for example, "111" into Succ Succ Succ Zero. Of
> course this doesn't work because parseP is ill-typed, but I'm not sure how
> to fix it. It seems that what I'm asking for is a function whose type is
> forall a. (Card a) => String -> a, which is problematic.
>
> Has anyone tried this before? I'm new to using Parsec and to parsing in
> general, so I apologize if this is a silly question. (Parsec is very
> impressive, by the way.)
>
> Thanks-
>
> Nathan Bloomfield
> University of Arkansas, Fayetteville
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>