I seem to constantly abuse TypeFamilies; what do i really want?
I've used TypeFamilies numerous times in code and library APIs to get more powerful and creative type-checking, and I seem to always use it in the same way that ends up feeling like abuse. For instance here's an example I started to sketch up for a talk I'm giving; this is to be a type-checked RPN calculator, used e.g. like `eval () (1,(2,((+),())))`: ``` {-# LANGUAGE TypeFamilies , MultiParamTypeClasses , FlexibleInstances , UndecidableInstances #-} type family EvaledStack x stack type instance EvaledStack Int st = (Int,st) type instance EvaledStack (Int -> x) (Int,st) = EvaledStack x st type family FinalStack string initialStack type instance FinalStack () st = st type instance FinalStack (x,xs) st = FinalStack xs (EvaledStack x st) class EvalStep x stack where evalStep :: x -> stack -> EvaledStack x stack instance (EvalStep x st)=> EvalStep (Int -> x) (Int,st) where evalStep f (int,st) = evalStep (f int) st instance EvalStep Int st where evalStep int st = (int,st) class Eval string initialStack where eval :: initialStack -> string -> FinalStack string initialStack instance Eval () st where eval st () = st instance (EvalStep x st, Eval xs (EvaledStack x st))=> Eval (x,xs) st where eval st (x, xs) = eval (evalStep x st) xs ``` The code above is just a WIP, but notice several things: 1) It's intended to be "closed" but I can't express that 2) I need to use UndecidableInstances for the nested type family instances, even though the recursion I'm doing is simple 3) The classes are "ugly" with arbitrary instance heads 4) If I want to support polymorphic operators/operands I need to use OverlappingInstances, which is another layer of hack 5) Users get an unhelpful error from the type-checker if their RPN expression is ill-typed I think what I'm trying to do is fundamentally pretty simple, but I only have the tools to do it in the very ad-hoc way I've described. I think the new closed type families help me here, but I'm wondering: - have there been any proposals or discussions about this use case, or a name given to it? - do closed type families provide an elegant solution and I just don't realize it yet? - do other people find themselves using this pattern as well, or have I just gotten caught up in a strange way of abusing these extensions? Thanks a lot, Brandon
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
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"
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
On Friday, March 14, 2014 5:19:40 PM UTC-4, Eric Walkingshaw 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
That's a great point, thanks. I'll have to remember to interrogate myself on that next time I find myself reaching for this pattern. I wonder if your version can be made to work for functions of any arity? But in most (maybe not all) cases I really don't want to be defining new types. Thanks, Brandon
That's a great point, thanks. I'll have to remember to interrogate
myself on that next time I find myself reaching for this pattern. I wonder if your version can be made to work for functions of any arity?
Since functions get their arguments from the stack in reverse order, this implementation actually already supports functions of any arity if you just follow it with an appropriate number of `F2 ($)` commands. First, here's a nicer eval function: eval :: Prog () (a,()) eval p = fst (prog p ()) And here's how to apply the 3-ary function `zipWith` and the 4-ary function `zipWith3`: > eval (Push [1..3] :. Push [4..6] :. Push (,) :. F2 zipWith :. F2 ($) :. End) [(4,1),(5,2),(6,3)] > eval (Push [1..3] :. Push [4..6] :. Push [7..9] :. Push (,,) :. F2 zipWith3 :. F2 ($) :. F2 ($) :. End) [(7,4,1),(8,5,2),(9,6,3)] -Eric
On Fri, 14 Mar 2014 22:19:40 +0100, Eric Walkingshaw
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
Of course, there's also:
start :: (() -> r) -> r start f = f ()
end :: (a, s) -> a end = fst
push :: s -> a -> ((a, s) -> r) -> r push s a f = f (a, s)
op2 :: (a -> b -> c) -> (a, (b, s)) -> ((c, s) -> r) -> r op2 o (a, (b, s)) f = f (a `o` b, s)
add, mul :: Num a => (a, (a, s)) -> ((a, s) -> r) -> r add = op2 (+) mul = op2 (*)
example :: Integer example = -- 35 start push 2 push 3 add push 7 mul end
participants (5)
-
Brandon Simmons -
Eric Walkingshaw -
Jake McArthur -
jberryman
-
Niklas Haas