From 63880f58258ed84a2f2b15e5acf1dc699912d0d9 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Fri, 5 Aug 2016 10:52:56 +0200 Subject: Better variadic lifting of builtins --- events/src/Events/Spec/Eval.hs | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs index 24cfeb6..ddb32e4 100644 --- a/events/src/Events/Spec/Eval.hs +++ b/events/src/Events/Spec/Eval.hs @@ -49,21 +49,22 @@ evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) -- bindE :: (m a -> b) -> Expr m (a ': Ctx b) (Fin b) -- bindE f = liftE $ bindE . f -type family Ctx f where - Ctx (a -> b) = (a ': Ctx b) - Ctx a = '[] +type family Ctx m f where + Ctx m (m a -> b) = (a ': Ctx m b) + Ctx m a = '[] -type family Fin f where - Fin (a -> b) = Fin b - Fin a = a +type family Fin m f where + Fin m (m a -> b) = Fin m b + Fin m (m a) = a + Fin m a = a class Bindable m b where - bindE :: (Val m a -> m b) -> Expr m (a ': Ctx b) (Fin b) + bindE :: (Val m a -> b) -> Expr m (a ': Ctx m b) (Fin m b) -instance {-# OVERLAPS #-} ((Val m b) ~ (m b), Applicative m, Bindable m c) => Bindable m (b -> c) where - bindE :: (Val m a -> m (b -> c)) -> Expr m (a ': b ': Ctx c) (Fin c) - bindE f = (EPri :: (Val m a -> Expr m (b ': Ctx c) (Fin c)) -> Expr m (a ': b ': Ctx c) (Fin c)) . ((bindE :: (Val m b -> m c) -> Expr m (b ': Ctx c) (Fin c)) . ) $ ((<*>) . f) +instance ((Val m b) ~ (m b), Applicative m, Bindable m c) => Bindable m (m b -> c) where + bindE :: (Val m a -> m b -> c) -> Expr m (a ': b ': Ctx m c) (Fin m c) + bindE f = (EPri :: (Val m a -> Expr m (b ': Ctx m c) (Fin m c)) -> Expr m (a ': b ': Ctx m c) (Fin m c)) . ((bindE :: (Val m b -> c) -> Expr m (b ': Ctx m c) (Fin m c)) . ) $ f -instance (Val m b ~ m b, Ctx b ~ '[], Fin b ~ b) => Bindable m b where +instance {-# OVERLAPPABLE #-} (Val m b ~ m b, Ctx m (m b) ~ '[], Fin m (m b) ~ b) => Bindable m (m b) where bindE :: (Val m a -> Val m b) -> Expr m '[a] b bindE = EPri . (EVal .) -- cgit v1.2.3