Two fun things with GADTs

1. Reifying class instances

Easy to do, and useful sometimes:

  data MyMonad m where
    MkMyMonad :: (Monad m) => MyMonad m

  myReturn :: MyMonad m -> a -> m a
  myReturn MkMyMonad = return

  myBind :: MyMonad m -> m a -> (a -> m b) -> m b
  myBind MkMyMonad = (>>=)

Note this may not yet be available in GHC CVS, see bug #1097046.


2. Casting among a limited set of types

  data Witness a where
    BoolWitness :: Witness Bool
    IntWitness :: Witness Int
    ListWitness :: Witness a -> Witness [a]

  data ComposeT p q a = MkComposeT {unComposeT p (q a)}

  witnessCast :: Witness a -> Witness b -> p a -> Maybe (p b)
  witnessCast BoolWitness BoolWitness pa = Just pa;
  witnessCast IntWitness IntWitness pa = Just pa;
  witnessCast (ListWitness wa) (ListWitness wb) pla = 
    fmap unComposeT (witnessCast wa wb (MkComposeT pla))
  witnessCast _ _ _ = Nothing;

  class Castable a where
    witness :: Witness a

  instance Castable Bool where
    witness = BoolWitness

  instance Castable Int where
    witness = IntWitness

  instance (Castable a) => Castable [a] where
    witness = ListWitness witness

  cast :: (Castable a,Castable b) => p a -> Maybe (p b)
  cast = witnessCast witness witness

  castOne :: (Castable a,Castable b) => a -> Maybe b
  castOne a = fmap runIdentity (cast (Identity a))

-- 
Ashley Yakeley, Seattle WA