[Haskell-cafe] Parsec and type level numerals

David Menendez dave at zednenem.com
Sat Dec 13 15:54:01 EST 2008

2008/12/13 Nathan Bloomfield <nbloomf at gmail.com>:
> 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. :)

This can be done with existential types. I think Oleg Kiselyov has an
example somewhere of a parser that determines the type of its output
from its input, but here's the basic idea:

data SomeCard = forall a. (Card a) => SomeCard a

Now you can define parseP :: Parser SomeCard

Unfortunately, all you know about the value inside the SomeCard is
that it's a member of the class Card, which may not be very helpful.
Depending on how general you want to be, you can bundle more
operations with SomeCard, or you can return a GADT that reflects the
type-level natural at the value level.

Dave Menendez <dave at zednenem.com>

More information about the Haskell-Cafe mailing list