[Haskell-cafe] type variable in class instance

[Sean Leather]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120911/50afdf31/attachment.htm>