compdata-0.5.3: Compositional Data Types

Portability non-portable (GHC Extensions) experimental Patrick Bahr None

Data.Comp.Sum

Description

This module provides the infrastructure to extend signatures.

Synopsis

Documentation

class sub :<: sup whereSource

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`.

Methods

inj :: sub a -> sup aSource

proj :: sup a -> Maybe (sub a)Source

Instances

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

data (f :+: g) e Source

Formal sum of signatures (functors).

Instances

 :<: 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 `ArbitraryF` are closed under forming sums. (NFDataF f, NFDataF g) => NFDataF (:+: f g) (EqF f, EqF g) => EqF (:+: f g) `EqF` is propagated through sums. (OrdF f, OrdF g) => OrdF (:+: f g) `OrdF` 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') (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

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

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

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

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

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.

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

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

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

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

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

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.

substHoles :: (Functor f, Functor g, f :<: g) => Cxt h' f v -> (v -> Cxt h g a) -> 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`.

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