On Tue, Sep 11, 2012 at 9:18 PM, Corentin Dupont wrote:
> That's very interesting.
> One problem is, if the set of event is closed, the set of possible data
> types is not (the user can choose any data type for a Message callback for
> example). I think this can be solved using a class instead of a GADT for
> "Type". One can also use a type witness?
>
Just a "bit" more complicated...
{-# LANGUAGE TypeFamilies, GADTs #-}
import Data.Typeable
import Unsafe.Coerce
data Player = Arrive | Leave deriving Show
newtype Message t = Message String deriving (Eq, Show)
data Type :: * -> * where
MessageT :: Typeable t => Proxy t -> Type (Message t)
PlayerT :: Type Player
data Proxy t
typeOfProxy :: Typeable t => Proxy t -> TypeRep
typeOfProxy x = typeOf (unproxy x)
where
unproxy :: Proxy t -> t
unproxy = undefined
data TEq :: * -> * -> * where
Refl :: TEq a a
teq :: Type a -> Type b -> Maybe (TEq a b)
teq (MessageT p) (MessageT q)
| typeOfProxy p == typeOfProxy q = Just (unsafeCoerce Refl)
teq PlayerT PlayerT = Just Refl
teq _ _ = Nothing
type family Data t :: *
type instance Data (Message t) = t
type instance Data Player = Int
data Event t = Event (Type t) t
data Handler where
Handler :: Event t -> (Data t -> IO ()) -> Handler
runHandler :: Eq t => Event t -> Data t -> Handler -> IO ()
runHandler (Event t e) d (Handler (Event u e') f) =
case teq t u of
Just Refl | e == e' -> f d
_ -> return ()
runHandlers :: Eq t => Event t -> Data t -> [Handler] -> IO ()
runHandlers e d hs = mapM_ (runHandler e d) hs
-- Replacement for viewEvent
instance Show (Event t) where
show (Event ty e) =
case ty of
MessageT t -> show e ++ " of type " ++ show (typeOfProxy t)
PlayerT -> "Player " ++ show e
messageEvent :: Typeable t => Proxy t -> String -> Event (Message t)
messageEvent t s = Event (MessageT t) (Message s)
playerEvent :: Player -> Event Player
playerEvent = Event PlayerT
-- Tests
int :: Proxy Int
int = undefined
event1 = messageEvent int "give me a number" -- No type signature
necessary!
handler1 = Handler event1 (\n -> putStrLn $ "Your number is: " ++ show n)
test1 = runHandlers event1 1 [handler1] -- Yields "Your number is: 1"
The Proxy type is not absolutely necessary, because you can use the type
directly. But I think the Proxy makes it clear that no (non-bottom) terms
of the type are expected.
Regards,
Sean
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
