[Haskell-cafe] Re: Typeclasses and GADT [Was: Regular Expressions without GADTs]

[Tomasz Zielonka]

On 10/27/05, oleg at pobox.com <oleg at pobox.com> wrote:
>
> Tomasz Zielonka wrote:
>
> > Speaking about casts, I was playing with using GADTs to create a
> > non-extensible version of Data.Typeable and Data.Dynamic.
> > I wonder if it's possible to write such a thing without GADTs (and
> > unsafeCoerce, which is used in Data.Dynamic, IIRC).
>
> Absolutely. Stephanie Weirich did that back in 2000 (actually, earlier:
> her paper, TypeSafe cast was presented at ICFP'00). The code does not
> use existentials -- only universals. BTW, if you don't plan to store
> your dynamics in a data structure (or plan to cast them to the same
> thing), then no explicit quantification is needed and the code becomes
> Haskell98. Here's her code for the cast, with slight
> embellishments.

This is cool! I thought that even if it was possible, the code would
be longer and less readable. It isn't.

I'm not sure I would be able to do everything I need to do
with this implementation of Dynamic (because I have some
other operations on Type), but I guess the answer is
True.

I've known about this paper, but I haven't read it yet. That was
a mistake :-)

> It should be pointed out that we can cast polymorphic
> lists and polymorphic functions.

I'm not sure I understand correctly, but I don't think you can
(toDyn const) and get a polymorhic function back from fromDyn.
I checked and I got an ambiguity error. Can you show an example?

> There is a different way to perform casting within a closed universe,
> see
>         http://www.mail-archive.com/haskell@haskell.org/msg13089.html

I'll check it out.

Best regards
Tomasz