cubix-compdata-1.0.1: Compositional Data Types for Cubix
Copyright(c) 2011 Patrick Bahr
LicenseBSD3
MaintainerPatrick Bahr <paba@diku.dk>
Stabilityexperimental
Portabilitynon-portable (GHC Extensions)
Safe HaskellNone
LanguageHaskell98

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 (f :: (* -> *) -> * -> *) :<: (g :: (* -> *) -> * -> *) infixl 5 Source #

Minimal complete definition

inj, proj

Instances

Instances details
f :<: f Source # 
Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a :: Type -> Type). f a :-> f a Source #

proj :: forall (a :: Type -> Type). NatM Maybe (f a) (f a) Source #

Mem f fs => f :<: (Sum fs) Source # 
Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a :: Type -> Type). f a :-> Sum fs a Source #

proj :: forall (a :: Type -> Type). NatM Maybe (Sum fs a) (f a) Source #

class f :<: Sum fs => f :-<: fs Source #

Instances

Instances details
f :<: Sum fs => f :-<: fs Source # 
Instance details

Defined in Data.Comp.Multi.Ops

data Sum (fs :: [(* -> *) -> * -> *]) h e Source #

Data type defining a sum of signatures.

It is inspired by modular reifiable matching, as described in

  • Oliveira, Bruno C. D. S., Shin-Cheng Mu, and Shu-Hung You. "Modular reifiable matching: a list-of-functors approach to two-level types." In Haskell Symposium, 2015.

except that this definition uses value-level integers (in the Elem datatype) in place of type-level naturals. It hence uses unsafeCoerce under the hood, but is type-safe if used through the public API. The result is that values of this type take constant memory with respect to the number of summands (unlike vanilla datatypes à la carte), and constant time to dereference (unlike modular reifiable matching). The representation is the bare minimum: an int representing the alternative, and pointer to the value.

Instances

Instances details
Mem f fs => f :<: (Sum fs) Source # 
Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a :: Type -> Type). f a :-> Sum fs a Source #

proj :: forall (a :: Type -> Type). NatM Maybe (Sum fs a) (f a) Source #

All (HasVars v) fs => HasVars v (Sum fs) Source # 
Instance details

Defined in Data.Comp.Multi.Variables

Methods

isVar :: forall (a :: Type -> Type). Sum fs a :=> Maybe v Source #

bindsVars :: forall (m :: Type -> Type) (a :: Type -> Type). Mapping m a => Sum fs a :=> m (Set v) Source #

All HFunctor fs => HFunctor (Sum fs) Source # 
Instance details

Defined in Data.Comp.Multi.Ops

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Sum fs f :-> Sum fs g Source #

(All HFoldable fs, All HFunctor fs) => HFoldable (Sum fs) Source # 
Instance details

Defined in Data.Comp.Multi.Ops

Methods

hfold :: Monoid m => Sum fs (K m) :=> m Source #

hfoldMap :: forall m (a :: Type -> Type). Monoid m => (a :=> m) -> Sum fs a :=> m Source #

hfoldr :: forall (a :: Type -> Type) b. (a :=> (b -> b)) -> b -> Sum fs a :=> b Source #

hfoldl :: forall b (a :: Type -> Type). (b -> a :=> b) -> b -> Sum fs a :=> b Source #

hfoldr1 :: (a -> a -> a) -> Sum fs (K a) :=> a Source #

hfoldl1 :: (a -> a -> a) -> Sum fs (K a) :=> a Source #

(All HTraversable fs, All HFoldable fs, All HFunctor fs) => HTraversable (Sum fs) Source # 
Instance details

Defined in Data.Comp.Multi.Ops

Methods

hmapM :: forall (m :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type). Monad m => NatM m a b -> NatM m (Sum fs a) (Sum fs b) Source #

htraverse :: forall (f :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type). Applicative f => NatM f a b -> NatM f (Sum fs a) (Sum fs b) Source #

All EqHF fs => EqHF (Sum fs) Source #

EqF is propagated through sums.

Instance details

Defined in Data.Comp.Multi.Equality

Methods

eqHF :: forall (g :: Type -> Type) i j. KEq g => Sum fs g i -> Sum fs g j -> Bool Source #

(All OrdHF fs, EqHF (Sum fs)) => OrdHF (Sum fs) Source #

OrdHF is propagated through sums.

Instance details

Defined in Data.Comp.Multi.Ordering

Methods

compareHF :: forall (a :: Type -> Type) i j. KOrd a => Sum fs a i -> Sum fs a j -> Ordering Source #

All ShowHF fs => ShowHF (Sum fs) Source # 
Instance details

Defined in Data.Comp.Multi.Show

(RemA f g, RemA (Sum fs) (Sum gs)) => RemA (Sum (f ': fs)) (Sum (g ': gs)) Source # 
Instance details

Defined in Data.Comp.Multi.Ops

Methods

remA :: forall (a :: Type -> Type). Sum (f ': fs) a :-> Sum (g ': gs) a Source #

(Generic (f e l), Generic (Sum fs e l)) => Generic (Sum (f ': fs) e l) Source # 
Instance details

Defined in Data.Comp.Multi.Derive.Generic

Associated Types

type Rep (Sum (f ': fs) e l) :: Type -> Type #

Methods

from :: Sum (f ': fs) e l -> Rep (Sum (f ': fs) e l) x #

to :: Rep (Sum (f ': fs) e l) x -> Sum (f ': fs) e l #

Generic (Sum ('[] :: [(Type -> Type) -> Type -> Type]) e l) Source # 
Instance details

Defined in Data.Comp.Multi.Derive.Generic

Associated Types

type Rep (Sum '[] e l) :: Type -> Type #

Methods

from :: Sum '[] e l -> Rep (Sum '[] e l) x #

to :: Rep (Sum '[] e l) x -> Sum '[] e l #

type Rep (Sum (f ': fs) e l) Source # 
Instance details

Defined in Data.Comp.Multi.Derive.Generic

type Rep (Sum (f ': fs) e l) = Rep (f e l) :+: Rep (Sum fs e l)
type Rep (Sum ('[] :: [(Type -> Type) -> Type -> Type]) e l) Source # 
Instance details

Defined in Data.Comp.Multi.Derive.Generic

type Rep (Sum ('[] :: [(Type -> Type) -> Type -> Type]) e l) = V1 :: Type -> Type

Projections for Signatures and Terms

proj :: (:<:) 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 projectn 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 deepProjectn instead.

Injections for Signatures and Terms

inj :: (:<:) 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 injectn 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 deepInjectn instead.

split :: f :=: Sum fs => (forall e l. Alts fs (HFix f) e (a l)) -> HFix 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.

type family IsSum (f :: (* -> *) -> * -> *) :: Bool where ... Source #

Equations

IsSum (Sum fs) = True 
IsSum f = False 

type NotSum f = IsSum f ~ False Source #

isNode :: forall f g h a l. f :<: g => Proxy f -> Cxt h g a l -> Bool Source #