compdata-0.9: Compositional Data Types

Copyright (c) 2011 Patrick Bahr BSD3 Patrick Bahr experimental non-portable (GHC Extensions) None Haskell98

Data.Comp.Multi.Sum

Description

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

Synopsis

# Documentation

type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g infixl 5 Source

A constraint `f :<: g` expresses that the signature `f` is subsumed by `g`, i.e. `f` can be used to construct elements in `g`.

data (f :+: g) h e infixr 6 Source

Data type defining coproducts.

Instances

 (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. (Desugar f h, Desugar g h) => Desugar ((:+:) * f g) h (HasVars f v0, HasVars g v0) => HasVars ((:+:) * f g) v DistAnn s p s' => DistAnn ((:+:) * f s) p ((:+:) * ((:&:) * f p) s') RemA s s' => RemA ((:+:) * ((:&:) * f p) s) ((:+:) * f s')

caseH :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c Source

Utility function to case on a higher-order functor sum, without exposing the internal representation of sums.

# Projections for Signatures and Terms

proj :: forall f g a. f :<: g => NatM Maybe (g a) (f a) 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.

deepProject :: (HTraversable g, g :<: f) => CxtFunM Maybe f 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.

# Injections for Signatures and Terms

inj :: forall f g a. f :<: g => f a :-> g a Source

inject :: g :<: f => g (Cxt h f a) :-> Cxt h f a Source

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.

deepInject :: (HFunctor g, g :<: f) => CxtFun g f Source

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.

split :: f :=: (f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a Source

# Injections and Projections for Constants

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

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 a Source

This function injects a whole context into another context.

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

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 a Source

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