>
 > On 26 Oct 2005 10:11:25 -0400, [EMAIL PROTECTED]
 > <[EMAIL PROTECTED]> wrote:
 > > Tomasz Zielonka <[EMAIL PROTECTED]> 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


Attachment: TI.lhs
Description: Binary data

Attachment: Typeable.lhs
Description: Binary data

Attachment: TypeCombinators.lhs
Description: Binary data

Attachment: GCast.lhs
Description: Binary data

Attachment: NatNum.lhs
Description: Binary data

_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to