Portability | non-portable (GHC Extensions) |
---|---|
Stability | experimental |
Maintainer | Patrick Bahr <paba@diku.dk> |
This module provides the infrastructure to extend signatures.
- class sub :<: sup where
- data (f :+: g) e
- proj2 :: forall f a g1 g2. (g1 :<: f, g2 :<: f) => f a -> Maybe (:+: g2 g1 a)
- proj3 :: forall f a g1 g2 g3. (g1 :<: f, g2 :<: f, g3 :<: f) => f a -> Maybe (:+: g3 (:+: g2 g1) a)
- proj4 :: forall f a g1 g2 g3 g4. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => f a -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a)
- proj5 :: forall f a g1 g2 g3 g4 g5. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => f a -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a)
- proj6 :: forall f a g1 g2 g3 g4 g5 g6. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => f a -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a)
- proj7 :: forall f a g1 g2 g3 g4 g5 g6 g7. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => f a -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a)
- proj8 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => f a -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a)
- proj9 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8 g9. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => f a -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a)
- proj10 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => f a -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a)
- project :: g :<: f => Cxt h f a -> Maybe (g (Cxt h f a))
- project2 :: forall h f a g1 g2. (g1 :<: f, g2 :<: f) => Cxt h f a -> Maybe (:+: g2 g1 (Cxt h f a))
- project3 :: forall h f a g1 g2 g3. (g1 :<: f, g2 :<: f, g3 :<: f) => Cxt h f a -> Maybe (:+: g3 (:+: g2 g1) (Cxt h f a))
- project4 :: forall h f a g1 g2 g3 g4. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => Cxt h f a -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) (Cxt h f a))
- project5 :: forall h f a g1 g2 g3 g4 g5. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => Cxt h f a -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) (Cxt h f a))
- project6 :: forall h f a g1 g2 g3 g4 g5 g6. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => Cxt h f a -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) (Cxt h f a))
- project7 :: forall h f a g1 g2 g3 g4 g5 g6 g7. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => Cxt h f a -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) (Cxt h f a))
- project8 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => Cxt h f a -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) (Cxt h f a))
- project9 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8 g9. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => Cxt h f a -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) (Cxt h f a))
- project10 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => Cxt h f a -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) (Cxt h f a))
- deepProject :: (Traversable g, g :<: f) => CxtFunM Maybe f g
- deepProject2 :: forall f g1 g2. (Traversable (:+: g2 g1), g1 :<: f, g2 :<: f) => CxtFunM Maybe f (:+: g2 g1)
- deepProject3 :: forall f g1 g2 g3. (Traversable (:+: g3 (:+: g2 g1)), g1 :<: f, g2 :<: f, g3 :<: f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))
- deepProject4 :: forall f g1 g2 g3 g4. (Traversable (:+: g4 (:+: g3 (:+: g2 g1))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))
- deepProject5 :: forall f g1 g2 g3 g4 g5. (Traversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => CxtFunM Maybe f (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))
- deepProject6 :: forall f g1 g2 g3 g4 g5 g6. (Traversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => CxtFunM Maybe f (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))
- deepProject7 :: forall f g1 g2 g3 g4 g5 g6 g7. (Traversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => CxtFunM Maybe f (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))
- deepProject8 :: forall f g1 g2 g3 g4 g5 g6 g7 g8. (Traversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => CxtFunM Maybe f (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))
- deepProject9 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9. (Traversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => CxtFunM Maybe f (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))
- deepProject10 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (Traversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => CxtFunM Maybe f (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))))
- inj2 :: forall g a f1 f2. (f1 :<: g, f2 :<: g) => :+: f2 f1 a -> g a
- inj3 :: forall g a f1 f2 f3. (f1 :<: g, f2 :<: g, f3 :<: g) => :+: f3 (:+: f2 f1) a -> g a
- inj4 :: forall g a f1 f2 f3 f4. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => :+: f4 (:+: f3 (:+: f2 f1)) a -> g a
- inj5 :: forall g a f1 f2 f3 f4 f5. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a -> g a
- inj6 :: forall g a f1 f2 f3 f4 f5 f6. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a -> g a
- inj7 :: forall g a f1 f2 f3 f4 f5 f6 f7. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a -> g a
- inj8 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a -> g a
- inj9 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8 f9. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a -> g a
- inj10 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a -> g a
- inject :: g :<: f => g (Cxt h f a) -> Cxt h f a
- inject2 :: forall h g a f1 f2. (f1 :<: g, f2 :<: g) => :+: f2 f1 (Cxt h g a) -> Cxt h g a
- inject3 :: forall h g a f1 f2 f3. (f1 :<: g, f2 :<: g, f3 :<: g) => :+: f3 (:+: f2 f1) (Cxt h g a) -> Cxt h g a
- inject4 :: forall h g a f1 f2 f3 f4. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => :+: f4 (:+: f3 (:+: f2 f1)) (Cxt h g a) -> Cxt h g a
- inject5 :: forall h g a f1 f2 f3 f4 f5. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) (Cxt h g a) -> Cxt h g a
- inject6 :: forall h g a f1 f2 f3 f4 f5 f6. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) (Cxt h g a) -> Cxt h g a
- inject7 :: forall h g a f1 f2 f3 f4 f5 f6 f7. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) (Cxt h g a) -> Cxt h g a
- inject8 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) (Cxt h g a) -> Cxt h g a
- inject9 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8 f9. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) (Cxt h g a) -> Cxt h g a
- inject10 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) (Cxt h g a) -> Cxt h g a
- deepInject :: (Functor g, g :<: f) => CxtFun g f
- deepInject2 :: forall g f1 f2. (Functor (:+: f2 f1), f1 :<: g, f2 :<: g) => CxtFun (:+: f2 f1) g
- deepInject3 :: forall g f1 f2 f3. (Functor (:+: f3 (:+: f2 f1)), f1 :<: g, f2 :<: g, f3 :<: g) => CxtFun (:+: f3 (:+: f2 f1)) g
- deepInject4 :: forall g f1 f2 f3 f4. (Functor (:+: f4 (:+: f3 (:+: f2 f1))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
- deepInject5 :: forall g f1 f2 f3 f4 f5. (Functor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
- deepInject6 :: forall g f1 f2 f3 f4 f5 f6. (Functor (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => CxtFun (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) g
- deepInject7 :: forall g f1 f2 f3 f4 f5 f6 f7. (Functor (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => CxtFun (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) g
- deepInject8 :: forall g f1 f2 f3 f4 f5 f6 f7 f8. (Functor (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => CxtFun (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) g
- deepInject9 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9. (Functor (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => CxtFun (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) g
- deepInject10 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (Functor (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => CxtFun (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))) g
- injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a
- injectConst2 :: (Functor f1, Functor f2, Functor g, f1 :<: g, f2 :<: g) => Const (f1 :+: f2) -> Cxt h g a
- injectConst3 :: (Functor f1, Functor f2, Functor f3, Functor g, f1 :<: g, f2 :<: g, f3 :<: g) => Const (f1 :+: (f2 :+: f3)) -> Cxt h g a
- projectConst :: (Functor g, g :<: f) => Cxt h f a -> Maybe (Const g)
- injectCxt :: (Functor g, g :<: f) => Cxt h' g (Cxt h f a) -> Cxt h f a
- liftCxt :: (Functor f, g :<: f) => g a -> Context f a
- substHoles :: (Functor f, Functor g, f :<: g) => Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
- substHoles' :: (Functor f, Functor g, f :<: g, Ord v) => Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
Documentation
Signature containment relation for automatic injections. The left-hand must
be an atomic signature, where as the right-hand side must have a list-like
structure. Examples include f :<: f :+: g
and g :<: f :+: (g :+: h)
,
non-examples include f :+: g :<: f :+: (g :+: h)
and
f :<: (f :+: g) :+: h
.
Formal sum of signatures (functors).
f :<: g => f :<: (:+: h g) | |
f :<: (:+: f g) | |
(Functor f, Functor g) => Functor (:+: f g) | |
(Foldable f, Foldable g) => Foldable (:+: f g) | |
(Traversable f, Traversable g) => Traversable (:+: f g) | |
(ShowF f, ShowF g) => ShowF (:+: f g) | |
(ArbitraryF f, ArbitraryF g) => ArbitraryF (:+: f g) | Instances of |
(NFDataF f, NFDataF g) => NFDataF (:+: f g) | |
(EqF f, EqF g) => EqF (:+: f g) |
|
(OrdF f, OrdF g) => OrdF (:+: f g) |
|
(HasVars f v0, HasVars g v0) => HasVars (:+: f g) v0 | |
(Desugar f g0, Desugar g g0) => Desugar (:+: f g) g0 | |
DistAnn s p s' => DistAnn (:+: f s) p (:+: (:&: f p) s') | |
RemA s s' => RemA (:+: (:&: f p) s) (:+: f s') | |
(Eq (f a), Eq (g a)) => Eq (:+: f g a) | |
(Ord (f a), Ord (g a)) => Ord (:+: f g a) | |
(Show (f a), Show (g a)) => Show (:+: f g a) |
Projections for Signatures and Terms
proj3 :: forall f a g1 g2 g3. (g1 :<: f, g2 :<: f, g3 :<: f) => f a -> Maybe (:+: g3 (:+: g2 g1) a)Source
proj4 :: forall f a g1 g2 g3 g4. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => f a -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a)Source
proj5 :: forall f a g1 g2 g3 g4 g5. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => f a -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a)Source
proj6 :: forall f a g1 g2 g3 g4 g5 g6. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => f a -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a)Source
proj7 :: forall f a g1 g2 g3 g4 g5 g6 g7. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => f a -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a)Source
proj8 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => f a -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a)Source
proj9 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8 g9. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => f a -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a)Source
proj10 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => f a -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a)Source
project :: g :<: f => Cxt h f a -> Maybe (g (Cxt h f a))Source
Project the outermost layer of a term to a sub signature. If the signature
g
is compound of n atomic signatures, use project
n instead.
project2 :: forall h f a g1 g2. (g1 :<: f, g2 :<: f) => Cxt h f a -> Maybe (:+: g2 g1 (Cxt h f a))Source
project3 :: forall h f a g1 g2 g3. (g1 :<: f, g2 :<: f, g3 :<: f) => Cxt h f a -> Maybe (:+: g3 (:+: g2 g1) (Cxt h f a))Source
project4 :: forall h f a g1 g2 g3 g4. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => Cxt h f a -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) (Cxt h f a))Source
project5 :: forall h f a g1 g2 g3 g4 g5. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => Cxt h f a -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) (Cxt h f a))Source
project6 :: forall h f a g1 g2 g3 g4 g5 g6. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => Cxt h f a -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) (Cxt h f a))Source
project7 :: forall h f a g1 g2 g3 g4 g5 g6 g7. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => Cxt h f a -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) (Cxt h f a))Source
project8 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => Cxt h f a -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) (Cxt h f a))Source
project9 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8 g9. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => Cxt h f a -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) (Cxt h f a))Source
project10 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => Cxt h f a -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) (Cxt h f a))Source
deepProject :: (Traversable g, g :<: f) => CxtFunM Maybe f gSource
Tries to coerce a termcontext to a termcontext over a sub-signature. If
the signature g
is compound of n atomic signatures, use
deepProject
n instead.
deepProject2 :: forall f g1 g2. (Traversable (:+: g2 g1), g1 :<: f, g2 :<: f) => CxtFunM Maybe f (:+: g2 g1)Source
deepProject3 :: forall f g1 g2 g3. (Traversable (:+: g3 (:+: g2 g1)), g1 :<: f, g2 :<: f, g3 :<: f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))Source
deepProject4 :: forall f g1 g2 g3 g4. (Traversable (:+: g4 (:+: g3 (:+: g2 g1))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))Source
deepProject5 :: forall f g1 g2 g3 g4 g5. (Traversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => CxtFunM Maybe f (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))Source
deepProject6 :: forall f g1 g2 g3 g4 g5 g6. (Traversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => CxtFunM Maybe f (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))Source
deepProject7 :: forall f g1 g2 g3 g4 g5 g6 g7. (Traversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => CxtFunM Maybe f (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))Source
deepProject8 :: forall f g1 g2 g3 g4 g5 g6 g7 g8. (Traversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => CxtFunM Maybe f (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))Source
deepProject9 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9. (Traversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => CxtFunM Maybe f (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))Source
deepProject10 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (Traversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))), g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => CxtFunM Maybe f (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))))Source
Injections for Signatures and Terms
inj4 :: forall g a f1 f2 f3 f4. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => :+: f4 (:+: f3 (:+: f2 f1)) a -> g aSource
inj5 :: forall g a f1 f2 f3 f4 f5. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a -> g aSource
inj6 :: forall g a f1 f2 f3 f4 f5 f6. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a -> g aSource
inj7 :: forall g a f1 f2 f3 f4 f5 f6 f7. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a -> g aSource
inj8 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a -> g aSource
inj9 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8 f9. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a -> g aSource
inj10 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a -> g aSource
inject :: g :<: f => g (Cxt h f a) -> Cxt h f aSource
Inject a term where the outermost layer is a sub signature. If the signature
g
is compound of n atomic signatures, use inject
n instead.
inject3 :: forall h g a f1 f2 f3. (f1 :<: g, f2 :<: g, f3 :<: g) => :+: f3 (:+: f2 f1) (Cxt h g a) -> Cxt h g aSource
inject4 :: forall h g a f1 f2 f3 f4. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => :+: f4 (:+: f3 (:+: f2 f1)) (Cxt h g a) -> Cxt h g aSource
inject5 :: forall h g a f1 f2 f3 f4 f5. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) (Cxt h g a) -> Cxt h g aSource
inject6 :: forall h g a f1 f2 f3 f4 f5 f6. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) (Cxt h g a) -> Cxt h g aSource
inject7 :: forall h g a f1 f2 f3 f4 f5 f6 f7. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) (Cxt h g a) -> Cxt h g aSource
inject8 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) (Cxt h g a) -> Cxt h g aSource
inject9 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8 f9. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) (Cxt h g a) -> Cxt h g aSource
inject10 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) (Cxt h g a) -> Cxt h g aSource
deepInject :: (Functor g, g :<: f) => CxtFun g fSource
Inject a term over a sub signature to a term over larger signature. If the
signature g
is compound of n atomic signatures, use deepInject
n
instead.
deepInject2 :: forall g f1 f2. (Functor (:+: f2 f1), f1 :<: g, f2 :<: g) => CxtFun (:+: f2 f1) gSource
deepInject3 :: forall g f1 f2 f3. (Functor (:+: f3 (:+: f2 f1)), f1 :<: g, f2 :<: g, f3 :<: g) => CxtFun (:+: f3 (:+: f2 f1)) gSource
deepInject4 :: forall g f1 f2 f3 f4. (Functor (:+: f4 (:+: f3 (:+: f2 f1))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) gSource
deepInject5 :: forall g f1 f2 f3 f4 f5. (Functor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) gSource
deepInject6 :: forall g f1 f2 f3 f4 f5 f6. (Functor (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => CxtFun (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) gSource
deepInject7 :: forall g f1 f2 f3 f4 f5 f6 f7. (Functor (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => CxtFun (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) gSource
deepInject8 :: forall g f1 f2 f3 f4 f5 f6 f7 f8. (Functor (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => CxtFun (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) gSource
deepInject9 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9. (Functor (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => CxtFun (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) gSource
deepInject10 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (Functor (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => CxtFun (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))) gSource
Injections and Projections for Constants
injectConst2 :: (Functor f1, Functor f2, Functor g, f1 :<: g, f2 :<: g) => Const (f1 :+: f2) -> Cxt h g aSource
injectConst3 :: (Functor f1, Functor f2, Functor f3, Functor g, f1 :<: g, f2 :<: g, f3 :<: g) => Const (f1 :+: (f2 :+: f3)) -> Cxt h g aSource
injectCxt :: (Functor g, g :<: f) => Cxt h' g (Cxt h f a) -> Cxt h f aSource
This function injects a whole context into another context.
liftCxt :: (Functor f, g :<: f) => g a -> Context f aSource
This function lifts the given functor to a context.