On 10/27/05, oleg@pobox.com
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