[Haskell-cafe] Parsec and type level numerals

[Reiner Pope]

On Sun, Dec 14, 2008 at 6:54 AM, David Menendez <dave at zednenem.com> wrote:
> 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>
> <http://www.eyrie.org/~zednenem/>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

Depending on what you actually want to do, you may be looking for Oleg
Kiselyov's reifyIntegral function, which he defines in the paper
"Functional Pearl: Implicit Configurations -- or Type Classes Reflect
the Value of Types" (at
http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf ). It has type
something like

reifyIntegral :: forall a. Int -> (forall n. Numeral n => n -> a) -> a

encoding n's existential type with continuation passing style.

Cheers,
Reiner