A benefit of using type families and type classes instead of GADTs for this kind of thing when you can is they are usually cheaper. You can often write code that inlines perfectly with former but ends up being some recursive function that will never inline with the latter.

- Jake

On Mar 14, 2014 5:20 PM, "Eric Walkingshaw" <walkiner@eecs.oregonstate.edu> wrote:
I'm not sure if this answers your questions, but I think this particular problem has a cleaner solution with GADTs:

    {-# LANGUAGE GADTs #-}
    
    data Cmd s t where
      Push :: a             -> Cmd s         (a,s)
      F1   :: (a -> b)      -> Cmd (a,s)     (b,s)
      F2   :: (a -> b -> c) -> Cmd (a,(b,s)) (c,s)
    
    data Prog s t where
      (:.) :: Cmd s t -> Prog t u -> Prog s u
      End  :: Prog s s
    
    infixr 5 :.
    
    cmd :: Cmd s t -> s -> t
    cmd (Push a) s         = (a, s)
    cmd (F1 f)   (a,s)     = (f a, s)
    cmd (F2 f)   (a,(b,s)) = (f a b, s)
    
    prog :: Prog s t -> s -> t
    prog (c :. p) s = prog p (cmd c s)
    prog End      s = s
    
    run :: Prog () t -> t
    run p = prog p ()

Then from GHCi:
    
    > run (Push 3 :. Push 4 :. F2 (+) :. F1 show :. End)
    ("7",())

Maybe you really want GADTs? :)

-Eric

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe