[Haskell-cafe] type variable in class instance

[Corentin Dupont]

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?

On Tue, Sep 11, 2012 at 8:09 PM, Sean Leather <leather at cs.uu.nl> wrote:

> On Tue, Sep 11, 2012 at 6:46 PM, David Menendez wrote:
>
> Mixing GADTs and Typeable seems like a bad idea. If you really don't
>> want to put viewEvent in the Event typeclass, but the class of events
>> is closed, you could use a GADT to witness the event type.
>
>
> On Tue, Sep 11, 2012 at 7:03 PM, Corentin Dupont wrote:
>
>> unfortunately it seems that I will be obliged to maintain 2 parallel
>> structures:
>> for each Event instance, I will have to add a ViewEvent element as well
>> carrying the same information:
>
> That's why I like the all-GADT solution...
>
>
> Inspired by David's suggestion, here's another version without Typeable.
> In Corentin's version, the switching back and forth between explicit and
> forgetful typing bothered me. This version never forgets types. Also,
> viewEvent is really an instance of Show, as I would expect. I don't see the
> extra maintenance burden mentioned by Corentin.
>
> {-# LANGUAGE TypeFamilies, GADTs #-}
>
> data Player = Arrive | Leave deriving Show
> newtype Message t = Message String deriving (Eq, Show)
>
> data Type :: * -> * where
>   Int    :: Type (Message Int)
>   String :: Type (Message String)
>   Player :: Type Player
>
> data TEq :: * -> * -> * where
>   Refl :: TEq a a
>
> teq :: Type a -> Type b -> Maybe (TEq a b)
> teq Int    Int    = Just Refl
> teq String String = Just Refl
> teq Player Player = 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
>       Int    -> show e ++ " of type Int"
>       String -> show e ++ " of type String"
>       Player -> "Player " ++ show e
>
> messageEvent :: Type (Message t) -> String -> Event (Message t)
> messageEvent t s = Event t (Message s)
>
> playerEvent :: Player -> Event Player
> playerEvent = Event Player
>
> -- Tests
>
> 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"
>
> Regards,
> Sean
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120911/31e212d0/attachment-0001.htm>