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

[oleg at 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. It should be pointed out that we can cast polymorphic
lists and polymorphic functions.

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

{-# OPTIONS -fglasgow-exts #-}

module CWeirich where

class CF a where
    cast :: CT b => a -> Maybe b

class CT b where
    cBool :: Bool -> Maybe b
    cBool = const Nothing
    cInt  :: Int  -> Maybe b
    cInt  = const Nothing
    cList :: CF a => [a] -> Maybe b
    cList = const Nothing
    cFun  :: (CT b1, CF a2) => (b1->a2) -> Maybe b
    cFun  = const Nothing

instance CF Bool where cast = cBool
instance CF Int  where cast = cInt
instance CF a => CF [a] where cast = cList
instance (CT b1, CF a2) => CF (b1->a2) where cast = cFun

instance CT Bool where cBool = Just
instance CT Int  where cInt  = Just
instance CT b => CT [b]  where cList x = mapM cast x
instance (CT b2, CF a1) => CT (a1->b2) where 
    cFun f = 
	let f' :: a1 -> Maybe b2
	    f' x   = maybe Nothing (cast . f) (cast x)
	    f'' x  = maybe undefined id (f' x)
	in maybe Nothing (const $ Just f'') (f' undefined)


-- This is a universal rather than existential type!
data Dyn = Dyn {fromDyn :: forall b. CT b => Maybe b}

toDyn :: CF a => a -> Dyn
toDyn a = Dyn (cast a)

td1 = toDyn True
td2 = toDyn [1::Int, 2,3]
td3 = toDyn not

tf1 = fromDyn td1 :: Maybe Bool
tf2 = fromDyn td1 :: Maybe Int
tf3 = fromDyn td2 :: Maybe [Int]
tf4 :: Maybe Bool = maybe Nothing (\f -> Just $ f True) (fromDyn td2)
tf5 :: Maybe Bool = maybe Nothing (\f -> Just $ f True) (fromDyn td3)
tf6 :: Maybe Int  = maybe Nothing (\f -> Just $ f True) (fromDyn td3)