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

On 26 Oct 2005 10:11:25 -0400, kahl@cas.mcmaster.ca wrote:

...

Tomasz Zielonka wrote Wed, 26 Oct 2005 13:37:29 +0200:

...

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).

It is possible to get even closer to Typeable by using the same interface --- which is sufficient for some applications.

Hmmm... but you use unsafeCoerce, don't you? ;-)

I might have been unclear about it - I didn't want to use unsafeCoerce. With unsafeCoerce you can easily implement Typeable/Dynamic without GADTs, don't you?

The misunderstanding was entirely on my side: I had not seen the previous discussion, but only been forwarded your last message by Jacques. Now I finally subscribed to haskell-cafe, too... My concern was more with the interface than with the implementation. I need ``TI'' (your ``Type'') to make some other things possible that are not possible with Data.Typeable, but also have a bunch of things that do work with Data.Typeable. With -ddump-minimal-imports, I see that most of my files import only (Typeable*(), gcast) from Data.Typeable --- only a fraction actually use TypeRep or typeOf*. My main point was that this common interface can be implemented also with the GADT implementation of Typeable, so there is no need to rewrite code based on that common interface. A seondary point was the use of separate types at separate kinds, corresponding to the separate Typeable* classes at separate kinds. Since your Type and my TI are essentially the same, your nice technique for the cast can of course be transferred --- while your Wrapper* types have a custom flavour, I use general type combinators that are useful also in other settings. These are essentially just the standard combinatory logic combinators (with some Haskell influence ;-): newtype I x =I x newtype K x y =K x newtype S f g x =S (f x (g x)) newtype Flip f x y =Flip (f y x) newtype B f g x =B (f (g x)) Unfortunately we do not have kind polymorphism, so we have to define variants for all the kind combinations we need. Naming these is a challenge --- I am still experimenting. (attached module TypeCombinators) The attached modules now don't use unsafeCoerce any more (thanks!), but still include all the higher-kinded material. Wolfram