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)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
