>> {-# OPTIONS -fglasgow-exts #-}
>>
>> module Main where
>>
>> import Data.IORef
>>
>> data T a where
>> Li:: Int -> T Int
>> Lb:: Bool -> T Bool
>> La:: a -> T a
>>
>> writeInt:: T a -> IORef a -> IO ()
>> writeInt v ref = case v of
>> ~(Li x) -> writeIORef ref (1::Int)
>>
>> readBool:: T a -> IORef a -> IO ()
>> readBool v ref = case v of
>> ~(Lb x) ->
>> readIORef ref >>= (print . not)
>>
>> tt::T a -> IO ()
>> tt v = case v of
>> ~(Li x) -> print "OK"
>>
>> main = do
>> tt (La undefined)
>> ref <- newIORef undefined
>> writeInt (La undefined) ref
>> readBool (La undefined) ref
This code is more intricate than
data Eq a b where Refl :: Eq a a
coerce :: Eq a b -> a -> b
coerce ~Refl x = x
but I think it amounts to exactly the same thing: ref and x are forced
to a particular type witnessed by the GADT.
But I think that something still can be squeezed out, strictness is not
absolutely necessary (see upcoming mail on this thread).
Regards,
apfelmus
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
