Copyright	(c) 2011 Patrick Bahr
License	BSD3
Maintainer	Patrick Bahr <paba@diku.dk>
Stability	experimental
Portability	non-portable (GHC Extensions)
Safe Haskell	None
Language	Haskell2010

Data.Comp.Multi.Sum

Contents

Projections for Signatures and Terms
Injections for Signatures and Terms
Injections and Projections for Constants

Description

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

Synopsis

class (f :: Fragment) :<: (g :: Fragment)
class f :<: Sum fs => (f :: Fragment) :-<: (fs :: Signature)
data Sum (fs :: Signature) (h :: Family) e
proj :: forall (a :: Family). (:<:) f g => NatM Maybe (g a) (f a)
project :: forall (g :: Fragment) (f :: Fragment) h (a :: Type -> Type). g :<: f => NatM Maybe (Cxt h f a) (g (Cxt h f a))
deepProject :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment). (HTraversable g, g :<: f) => CxtFunM Maybe f g
inj :: forall (a :: Family). (:<:) f g => f a :-> g a
inject :: forall (g :: Fragment) (f :: Fragment) h (a :: Type -> Type). g :<: f => g (Cxt h f a) :-> Cxt h f a
deepInject :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment). (HFunctor g, g :<: f) => CxtFun g f
split :: forall (f :: Fragment) (fs :: Signature) a. f :=: Sum fs => (forall e l. Alts fs (HFix f) e (a l)) -> HFix f :-> a
injectConst :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment) h (a :: Type -> Type). (HFunctor g, g :<: f) => Const g :-> Cxt h f a
projectConst :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment) h (a :: Type -> Type). (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)
injectCxt :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment) h' h (a :: Type -> Type). (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a
liftCxt :: forall (f :: (Type -> Type) -> Type -> Type) (g :: Fragment) (a :: Family). (HFunctor f, g :<: f) => g a :-> Context f a
substHoles :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (v :: Type -> Type) h (a :: Type -> Type) h'. (HFunctor f, HFunctor g, f :<: g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a
type family IsSum (f :: Node) :: Bool where ...
type NotSum (f :: Node) = IsSum f ~ 'False
isNode :: forall (f :: Fragment) (g :: Fragment) h (a :: Type -> Type) l. f :<: g => Cxt h g a l -> Bool

Documentation

class (f :: Fragment) :<: (g :: Fragment) 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 :: Family). f a :-> f a Source # proj :: forall (a :: Family). 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 :: Family). f a :-> Sum fs a Source # proj :: forall (a :: Family). NatM Maybe (Sum fs a) (f a) Source #
(f :<: Sum fs, Default a) => f :<: (Sum fs :&: a) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods inj :: forall (a0 :: Family). f a0 :-> (Sum fs :&: a) a0 Source # proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) (f a0) Source #
f :<: Sum fs => (f :&: a) :<: (Sum fs :&: a) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods inj :: forall (a0 :: Family). (f :&: a) a0 :-> (Sum fs :&: a) a0 Source # proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) ((f :&: a) a0) Source #

class f :<: Sum fs => (f :: Fragment) :-<: (fs :: Signature) Source #

Instances

Instances details

f :<: Sum fs => f :-<: fs Source #
Instance details Defined in Data.Comp.Multi.Ops

data Sum (fs :: Signature) (h :: Family) 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 :: Family). f a :-> Sum fs a Source #

proj :: forall (a :: Family). 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 :: Family). Sum fs a :=> Maybe v Source #

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

(f :<: Sum fs, Default a) => f :<: (Sum fs :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a0 :: Family). f a0 :-> (Sum fs :&: a) a0 Source #

proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) (f a0) Source #

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

Instance details

Defined in Data.Comp.Multi.ConstrName

Methods

constrNameHF :: forall (e :: Family) l. Sum fs e l -> String Source #

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

Instance details

Defined in Data.Comp.Multi.Show

Methods

showHF :: Alg (Sum fs) (K String) Source #

showHF' :: Sum fs (K String) :=> String 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 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 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 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 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 #

(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 :: Family). Sum (f ': fs) a :-> Sum (g ': gs) a Source #

f :<: Sum fs => (f :&: a) :<: (Sum fs :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a0 :: Family). (f :&: a) a0 :-> (Sum fs :&: a) a0 Source #

proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) ((f :&: a) a0) 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)
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)

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 ('[] :: [Fragment]) e l) Source #

Instance details

Defined in Data.Comp.Multi.Derive.Generic

Associated Types

type Rep (Sum ('[] :: [Fragment]) e l)
Instance details Defined in Data.Comp.Multi.Derive.Generic type Rep (Sum ('[] :: [Fragment]) e l) = V1 :: Type -> Type

Methods

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

to :: Rep (Sum ('[] :: [Fragment]) e l) x -> Sum ('[] :: [Fragment]) 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 ('[] :: [Fragment]) e l) Source #

Instance details

Defined in Data.Comp.Multi.Derive.Generic

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

Projections for Signatures and Terms

proj :: forall (a :: Family). (:<:) f g => NatM Maybe (g a) (f a) Source #

project :: forall (g :: Fragment) (f :: Fragment) h (a :: Type -> Type). 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 :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment). (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 :: forall (a :: Family). (:<:) f g => f a :-> g a Source #

inject :: forall (g :: Fragment) (f :: Fragment) h (a :: Type -> Type). 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 :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment). (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 :: forall (f :: Fragment) (fs :: Signature) a. f :=: Sum fs => (forall e l. Alts fs (HFix f) e (a l)) -> HFix f :-> a Source #

Injections and Projections for Constants

injectConst :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment) h (a :: Type -> Type). (HFunctor g, g :<: f) => Const g :-> Cxt h f a Source #

projectConst :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment) h (a :: Type -> Type). (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g) Source #

injectCxt :: forall (g :: (Type -> Type) -> Type -> Type) (f :: Fragment) h' h (a :: Type -> Type). (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 :: forall (f :: (Type -> Type) -> Type -> Type) (g :: Fragment) (a :: Family). (HFunctor f, g :<: f) => g a :-> Context f a Source #

This function lifts the given functor to a context.

substHoles :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (v :: Type -> Type) h (a :: Type -> Type) h'. (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 :: Node) :: Bool where ... Source #

Equations

IsSum (Sum fs) = 'True
IsSum f = 'False

type NotSum (f :: Node) = IsSum f ~ 'False Source #

isNode :: forall (f :: Fragment) (g :: Fragment) h (a :: Type -> Type) l. f :<: g => Cxt h g a l -> Bool Source #

Call like isNode @f x