Portability | non-portable (GHC Extensions) |
---|---|
Stability | experimental |
Maintainer | Tom Hvitved <hvitved@diku.dk> |
Safe Haskell | None |
This module provides the infrastructure to extend signatures.
- class sub :<: sup where
- data (f :+: g) a b
- proj2 :: forall f a b g1 g2. (:<: g1 f, :<: g2 f) => f a b -> Maybe (:+: g2 g1 a b)
- proj3 :: forall f a b g1 g2 g3. (:<: g1 f, :<: g2 f, :<: g3 f) => f a b -> Maybe (:+: g3 (:+: g2 g1) a b)
- proj4 :: forall f a b g1 g2 g3 g4. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a b)
- proj5 :: forall f a b g1 g2 g3 g4 g5. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a b)
- proj6 :: forall f a b g1 g2 g3 g4 g5 g6. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => f a b -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a b)
- proj7 :: forall f a b g1 g2 g3 g4 g5 g6 g7. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => f a b -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a b)
- proj8 :: forall f a b 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 b -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a b)
- proj9 :: forall f a b 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 b -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a b)
- proj10 :: forall f a b 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 b -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a b)
- project :: g :<: f => Cxt h f a b -> Maybe (g a (Cxt h f a b))
- project2 :: forall h f a b g1 g2. (:<: g1 f, :<: g2 f) => Cxt h f a b -> Maybe (:+: g2 g1 a (Cxt h f a b))
- project3 :: forall h f a b g1 g2 g3. (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a b -> Maybe (:+: g3 (:+: g2 g1) a (Cxt h f a b))
- project4 :: forall h f a b g1 g2 g3 g4. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Cxt h f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a (Cxt h f a b))
- project5 :: forall h f a b g1 g2 g3 g4 g5. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Cxt h f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a (Cxt h f a b))
- project6 :: forall h f a b g1 g2 g3 g4 g5 g6. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Cxt h f a b -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a (Cxt h f a b))
- project7 :: forall h f a b 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 b -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a (Cxt h f a b))
- project8 :: forall h f a b 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 b -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a (Cxt h f a b))
- project9 :: forall h f a b 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 b -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a (Cxt h f a b))
- project10 :: forall h f a b 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 b -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a (Cxt h f a b))
- deepProject :: (Ditraversable g, g :<: f) => Term f -> Maybe (Term g)
- deepProject2 :: forall f g1 g2. (Ditraversable (:+: g2 g1), :<: g1 f, :<: g2 f) => Term f -> Maybe (Term (:+: g2 g1))
- deepProject3 :: forall f g1 g2 g3. (Ditraversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => Term f -> Maybe (Term (:+: g3 (:+: g2 g1)))
- deepProject4 :: forall f g1 g2 g3 g4. (Ditraversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Term f -> Maybe (Term (:+: g4 (:+: g3 (:+: g2 g1))))
- deepProject5 :: forall f g1 g2 g3 g4 g5. (Ditraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Term f -> Maybe (Term (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))
- deepProject6 :: forall f g1 g2 g3 g4 g5 g6. (Ditraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Term f -> Maybe (Term (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))
- deepProject7 :: forall f g1 g2 g3 g4 g5 g6 g7. (Ditraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Term f -> Maybe (Term (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))
- deepProject8 :: forall f g1 g2 g3 g4 g5 g6 g7 g8. (Ditraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Term f -> Maybe (Term (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))
- deepProject9 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9. (Ditraversable (:+: 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) => Term f -> Maybe (Term (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))))
- deepProject10 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (Ditraversable (:+: 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) => Term f -> Maybe (Term (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))))
- inj2 :: forall g a b f1 f2. (:<: f1 g, :<: f2 g) => :+: f2 f1 a b -> g a b
- inj3 :: forall g a b f1 f2 f3. (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a b -> g a b
- inj4 :: forall g a b f1 f2 f3 f4. (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a b -> g a b
- inj5 :: forall g a b f1 f2 f3 f4 f5. (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a b -> g a b
- inj6 :: forall g a b 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 b -> g a b
- inj7 :: forall g a b 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 b -> g a b
- inj8 :: forall g a b 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 b -> g a b
- inj9 :: forall g a b 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 b -> g a b
- inj10 :: forall g a b 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 b -> g a b
- inject :: g :<: f => g a (Cxt h f a b) -> Cxt h f a b
- inject' :: (Difunctor g, g :<: f) => g (Cxt h f a b) (Cxt h f a b) -> Cxt h f a b
- inject2 :: forall h g a b f1 f2. (:<: f1 g, :<: f2 g) => :+: f2 f1 a (Cxt h g a b) -> Cxt h g a b
- inject3 :: forall h g a b f1 f2 f3. (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a (Cxt h g a b) -> Cxt h g a b
- inject4 :: forall h g a b f1 f2 f3 f4. (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a (Cxt h g a b) -> Cxt h g a b
- inject5 :: forall h g a b f1 f2 f3 f4 f5. (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a (Cxt h g a b) -> Cxt h g a b
- inject6 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
- inject7 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
- inject8 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
- inject9 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
- inject10 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
- deepInject :: (Difunctor g, g :<: f) => Term g -> Term f
- deepInject2 :: forall g f1 f2. (Difunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
- deepInject3 :: forall g f1 f2 f3. (Difunctor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
- deepInject4 :: forall g f1 f2 f3 f4. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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
- injectCxt :: (Difunctor g, g :<: f) => Cxt h g a (Cxt h f a b) -> Cxt h f a b
- liftCxt :: (Difunctor f, g :<: f) => g a b -> Cxt Hole f a b
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 (difunctors).
:<: f g => f :<: (:+: h g) | |
f :<: (:+: f g) | |
(Difunctor f, Difunctor g) => Difunctor (:+: f g) | |
(Ditraversable f, Ditraversable g) => Ditraversable (:+: f g) | |
(EqD f, EqD g) => EqD (:+: f g) |
|
(OrdD f, OrdD g) => OrdD (:+: f g) |
|
(ShowD f, ShowD g) => ShowD (:+: f g) | |
(Desugar f g0, Desugar g0 g0) => Desugar (:+: f g0) g0 | |
DistAnn s p s' => DistAnn (:+: f s) p (:+: (:&: f p) s') | |
RemA s s' => RemA (:+: (:&: f p) s) (:+: f s') | |
(Eq (f a b), Eq (g a b)) => Eq (:+: f g a b) | |
(Ord (f a b), Ord (g a b)) => Ord (:+: f g a b) | |
(Show (f a b), Show (g a b)) => Show (:+: f g a b) |
Projections for Signatures and Terms
proj3 :: forall f a b g1 g2 g3. (:<: g1 f, :<: g2 f, :<: g3 f) => f a b -> Maybe (:+: g3 (:+: g2 g1) a b)Source
proj4 :: forall f a b g1 g2 g3 g4. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a b)Source
proj5 :: forall f a b g1 g2 g3 g4 g5. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a b)Source
proj6 :: forall f a b g1 g2 g3 g4 g5 g6. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => f a b -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a b)Source
proj7 :: forall f a b g1 g2 g3 g4 g5 g6 g7. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => f a b -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a b)Source
proj8 :: forall f a b 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 b -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a b)Source
proj9 :: forall f a b 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 b -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a b)Source
proj10 :: forall f a b 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 b -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a b)Source
project :: g :<: f => Cxt h f a b -> Maybe (g a (Cxt h f a b))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 b g1 g2. (:<: g1 f, :<: g2 f) => Cxt h f a b -> Maybe (:+: g2 g1 a (Cxt h f a b))Source
project3 :: forall h f a b g1 g2 g3. (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a b -> Maybe (:+: g3 (:+: g2 g1) a (Cxt h f a b))Source
project4 :: forall h f a b g1 g2 g3 g4. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Cxt h f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a (Cxt h f a b))Source
project5 :: forall h f a b g1 g2 g3 g4 g5. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Cxt h f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a (Cxt h f a b))Source
project6 :: forall h f a b g1 g2 g3 g4 g5 g6. (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Cxt h f a b -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a (Cxt h f a b))Source
project7 :: forall h f a b 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 b -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a (Cxt h f a b))Source
project8 :: forall h f a b 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 b -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a (Cxt h f a b))Source
project9 :: forall h f a b 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 b -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a (Cxt h f a b))Source
project10 :: forall h f a b 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 b -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a (Cxt h f a b))Source
deepProject :: (Ditraversable g, g :<: f) => Term f -> Maybe (Term g)Source
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. (Ditraversable (:+: g2 g1), :<: g1 f, :<: g2 f) => Term f -> Maybe (Term (:+: g2 g1))Source
deepProject3 :: forall f g1 g2 g3. (Ditraversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => Term f -> Maybe (Term (:+: g3 (:+: g2 g1)))Source
deepProject4 :: forall f g1 g2 g3 g4. (Ditraversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Term f -> Maybe (Term (:+: g4 (:+: g3 (:+: g2 g1))))Source
deepProject5 :: forall f g1 g2 g3 g4 g5. (Ditraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Term f -> Maybe (Term (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))Source
deepProject6 :: forall f g1 g2 g3 g4 g5 g6. (Ditraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Term f -> Maybe (Term (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))Source
deepProject7 :: forall f g1 g2 g3 g4 g5 g6 g7. (Ditraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Term f -> Maybe (Term (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))Source
deepProject8 :: forall f g1 g2 g3 g4 g5 g6 g7 g8. (Ditraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Term f -> Maybe (Term (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))Source
deepProject9 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9. (Ditraversable (:+: 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) => Term f -> Maybe (Term (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))))Source
deepProject10 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (Ditraversable (:+: 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) => Term f -> Maybe (Term (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))))Source
Injections for Signatures and Terms
inj3 :: forall g a b f1 f2 f3. (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a b -> g a bSource
inj4 :: forall g a b f1 f2 f3 f4. (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a b -> g a bSource
inj5 :: forall g a b f1 f2 f3 f4 f5. (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a b -> g a bSource
inj6 :: forall g a b 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 b -> g a bSource
inj7 :: forall g a b 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 b -> g a bSource
inj8 :: forall g a b 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 b -> g a bSource
inj9 :: forall g a b 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 b -> g a bSource
inj10 :: forall g a b 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 b -> g a bSource
inject :: g :<: f => g a (Cxt h f a b) -> Cxt h f a bSource
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.
inject' :: (Difunctor g, g :<: f) => g (Cxt h f a b) (Cxt h f a b) -> Cxt h f a bSource
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.
inject2 :: forall h g a b f1 f2. (:<: f1 g, :<: f2 g) => :+: f2 f1 a (Cxt h g a b) -> Cxt h g a bSource
inject3 :: forall h g a b f1 f2 f3. (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a (Cxt h g a b) -> Cxt h g a bSource
inject4 :: forall h g a b f1 f2 f3 f4. (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a (Cxt h g a b) -> Cxt h g a bSource
inject5 :: forall h g a b f1 f2 f3 f4 f5. (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a (Cxt h g a b) -> Cxt h g a bSource
inject6 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a bSource
inject7 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a bSource
inject8 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a bSource
inject9 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a bSource
inject10 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a bSource
deepInject :: (Difunctor g, g :<: f) => Term g -> Term 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. (Difunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) gSource
deepInject3 :: forall g f1 f2 f3. (Difunctor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) gSource
deepInject4 :: forall g f1 f2 f3 f4. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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. (Difunctor (:+: 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