compdata-0.9: Compositional Data Types

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

Data.Comp.Sum

Description

This module provides the infrastructure to extend signatures.

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

type (:=:) f g = (f :<: g, g :<: f) infixl 5 Source

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

Formal sum of signatures (functors).

Instances

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

caseF :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b Source

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

data Proxy a Source

Constructors

 P

# Projections for Signatures and Terms

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

deepProject :: (Traversable 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.

project_ :: SigFunM Maybe f g -> 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.

deepProject_ :: Traversable g => SigFunM Maybe f g -> 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 :: (Functor 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.

inject_ :: SigFun 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_ :: Functor g => SigFun 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 :: (Functor g, g :<: f) => Const g -> Cxt h f a Source

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

This function injects a whole context into another context.

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

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

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