compdata-0.5.1: Compositional Data Types

Portability non-portable (GHC Extensions) experimental Patrick Bahr

Data.Comp.Multi.Sum

Description

This module defines sums on signatures. All definitions are generalised versions of those in Data.Comp.Sum.

Synopsis

# Documentation

class sub :<: sup whereSource

The subsumption relation.

Methods

inj :: sub a :-> sup aSource

proj :: NatM Maybe (sup a) (sub a)Source

Instances

 f :<: f f :<: g => f :<: (:+: h g) f :<: (:+: f g)

data (f :+: g) h e Source

Data type defining coproducts.

Instances

 f :<: g => f :<: (:+: h g) f :<: (:+: f g) (HFunctor f, HFunctor g) => HFunctor (:+: f g) (HFoldable f, HFoldable g) => HFoldable (:+: f g) (HTraversable f, HTraversable g) => HTraversable (:+: f g) (ShowHF f, ShowHF g) => ShowHF (:+: f g) (EqHF f, EqHF g) => EqHF (:+: f g) `EqF` is propagated through sums. (OrdHF f, OrdHF g) => OrdHF (:+: f g) `OrdHF` is propagated through sums. (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')

# Projections for Signatures and Terms

proj2 :: forall f i a g1 g2. (g1 :<: f, g2 :<: f) => f a i -> Maybe (:+: g2 g1 a i)Source

proj3 :: forall f i a g1 g2 g3. (g1 :<: f, g2 :<: f, g3 :<: f) => f a i -> Maybe (:+: g3 (:+: g2 g1) a i)Source

proj4 :: forall f i a g1 g2 g3 g4. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => f a i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a i)Source

proj5 :: forall f i a g1 g2 g3 g4 g5. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => f a i -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a i)Source

proj6 :: forall f i a g1 g2 g3 g4 g5 g6. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => f a i -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a i)Source

proj7 :: forall f i a g1 g2 g3 g4 g5 g6 g7. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => f a i -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a i)Source

proj8 :: forall f i 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 i -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a i)Source

proj9 :: forall f i 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 i -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a i)Source

proj10 :: forall f i 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 i -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a i)Source

project :: g :<: f => NatM Maybe (Cxt h f a) (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 i g1 g2. (g1 :<: f, g2 :<: f) => Cxt h f a i -> Maybe (:+: g2 g1 (Cxt h f a) i)Source

project3 :: forall h f a i g1 g2 g3. (g1 :<: f, g2 :<: f, g3 :<: f) => Cxt h f a i -> Maybe (:+: g3 (:+: g2 g1) (Cxt h f a) i)Source

project4 :: forall h f a i g1 g2 g3 g4. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => Cxt h f a i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) (Cxt h f a) i)Source

project5 :: forall h f a i g1 g2 g3 g4 g5. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => Cxt h f a i -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) (Cxt h f a) i)Source

project6 :: forall h f a i g1 g2 g3 g4 g5 g6. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => Cxt h f a i -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) (Cxt h f a) i)Source

project7 :: forall h f a i 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 i -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) (Cxt h f a) i)Source

project8 :: forall h f a i 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 i -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) (Cxt h f a) i)Source

project9 :: forall h f a i 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 i -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) (Cxt h f a) i)Source

project10 :: forall h f a i 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 i -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) (Cxt h f a) i)Source

deepProject :: (HTraversable 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. (HTraversable (:+: g2 g1), g1 :<: f, g2 :<: f) => CxtFunM Maybe f (:+: g2 g1)Source

deepProject3 :: forall f g1 g2 g3. (HTraversable (:+: g3 (:+: g2 g1)), g1 :<: f, g2 :<: f, g3 :<: f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))Source

deepProject4 :: forall f g1 g2 g3 g4. (HTraversable (:+: 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. (HTraversable (:+: 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. (HTraversable (:+: 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. (HTraversable (:+: 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. (HTraversable (:+: 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. (HTraversable (:+: 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. (HTraversable (:+: 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

inj2 :: forall g a i f1 f2. (f1 :<: g, f2 :<: g) => :+: f2 f1 a i -> g a iSource

inj3 :: forall g a i f1 f2 f3. (f1 :<: g, f2 :<: g, f3 :<: g) => :+: f3 (:+: f2 f1) a i -> g a iSource

inj4 :: forall g a i f1 f2 f3 f4. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => :+: f4 (:+: f3 (:+: f2 f1)) a i -> g a iSource

inj5 :: forall g a i f1 f2 f3 f4 f5. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a i -> g a iSource

inj6 :: forall g a i 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 i -> g a iSource

inj7 :: forall g a i 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 i -> g a iSource

inj8 :: forall g a i 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 i -> g a iSource

inj9 :: forall g a i 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 i -> g a iSource

inj10 :: forall g a i 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 i -> g a iSource

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.

inject2 :: forall h g a i f1 f2. (f1 :<: g, f2 :<: g) => :+: f2 f1 (Cxt h g a) i -> Cxt h g a iSource

inject3 :: forall h g a i f1 f2 f3. (f1 :<: g, f2 :<: g, f3 :<: g) => :+: f3 (:+: f2 f1) (Cxt h g a) i -> Cxt h g a iSource

inject4 :: forall h g a i f1 f2 f3 f4. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => :+: f4 (:+: f3 (:+: f2 f1)) (Cxt h g a) i -> Cxt h g a iSource

inject5 :: forall h g a i f1 f2 f3 f4 f5. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) (Cxt h g a) i -> Cxt h g a iSource

inject6 :: forall h g a i 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) i -> Cxt h g a iSource

inject7 :: forall h g a i 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) i -> Cxt h g a iSource

inject8 :: forall h g a i 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) i -> Cxt h g a iSource

inject9 :: forall h g a i 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) i -> Cxt h g a iSource

inject10 :: forall h g a i 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) i -> Cxt h g a iSource

deepInject :: (HFunctor 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. (HFunctor (:+: f2 f1), f1 :<: g, f2 :<: g) => CxtFun (:+: f2 f1) gSource

deepInject3 :: forall g f1 f2 f3. (HFunctor (:+: f3 (:+: f2 f1)), f1 :<: g, f2 :<: g, f3 :<: g) => CxtFun (:+: f3 (:+: f2 f1)) gSource

deepInject4 :: forall g f1 f2 f3 f4. (HFunctor (:+: 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. (HFunctor (:+: 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. (HFunctor (:+: 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. (HFunctor (:+: 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. (HFunctor (:+: 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. (HFunctor (:+: 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. (HFunctor (:+: 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

injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f aSource

injectConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g) => Const (f1 :+: f2) :-> Cxt h g aSource

injectConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, f1 :<: g, f2 :<: g, f3 :<: g) => Const (f1 :+: (f2 :+: f3)) :-> Cxt h g aSource

projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)Source

injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f aSource

This function injects a whole context into another context.

liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f aSource

This function lifts the given functor to a context.

substHoles :: (HFunctor f, HFunctor g, f :<: g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g aSource

This function applies the given context with hole type `a` to a family `f` of contexts (possibly terms) indexed by `a`. That is, each hole `h` is replaced by the context `f h`.