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

[kahl at cas.mcmaster.ca]

 >
 > On 26 Oct 2005 10:11:25 -0400, kahl at cas.mcmaster.ca
 > <kahl at cas.mcmaster.ca> wrote:
 > > Tomasz Zielonka <tomasz.zielonka at gmail.com> 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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: TI.lhs
Type: application/octet-stream
Size: 3192 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20051026/0ef3b30d/TI.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Typeable.lhs
Type: application/octet-stream
Size: 5568 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20051026/0ef3b30d/Typeable.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: TypeCombinators.lhs
Type: application/octet-stream
Size: 2364 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20051026/0ef3b30d/TypeCombinators.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: GCast.lhs
Type: application/octet-stream
Size: 877 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20051026/0ef3b30d/GCast.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: NatNum.lhs
Type: application/octet-stream
Size: 146 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20051026/0ef3b30d/NatNum.obj
-------------- next part --------------