Data.Comp.Multi.Ops

This module provides operators on higher-order functors. All definitions are generalised versions of those in Data.Comp.Ops.

Documentation

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

Data type defining coproducts.

Constructors

Inl (f h e)

Inr (g h e)

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

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

type family Elem f g :: Emb

Equations

Elem f f = Found Here

Elem (f1 :+: f2) g = Sum' (Elem f1 g) (Elem f2 g)

Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)

Elem f g = NotFound

type family Choose e1 r :: Emb

Equations

Choose (Found x) (Found y) = Ambiguous

Choose Ambiguous y = Ambiguous

Choose x Ambiguous = Ambiguous

Choose (Found x) y = Found (Le x)

Choose x (Found y) = Found (Ri y)

Choose x y = NotFound

type family Sum' e1 r :: Emb

Equations

Sum' (Found x) (Found y) = Found (Sum x y)

Sum' Ambiguous y = Ambiguous

Sum' x Ambiguous = Ambiguous

Sum' NotFound y = NotFound

Sum' x NotFound = NotFound

data Proxy a

Constructors

P

class Subsume e f g where

Methods

inj' :: Proxy e -> f a :-> g a

prj' :: Proxy e -> NatM Maybe (g a) (f a)

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

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

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

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

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

spl :: f :=: (f1 :+: f2) => (f1 a :-> b) -> (f2 a :-> b) -> f a :-> b

data (f :*: g) a infixr 8

Constructors

(f a) :*: (g a) infixr 8

fst :: (f :*: g) a -> f a

snd :: (f :*: g) a -> g a

data (f :&: a) g e infixr 7

This data type adds a constant product to a signature. Alternatively, this could have also been defined as

data (f :&: a) (g ::  * -> *) e = f g e :&: a e

This is too general, however, for example for productHHom.

Constructors

(f g e) :&: a infixr 7

Instances

DistAnn f p ((:&:) * f p)

HFunctor f => HFunctor ((:&:) * f a)

HFoldable f => HFoldable ((:&:) * f a)

HTraversable f => HTraversable ((:&:) * f a)

(ShowHF f, Show p) => ShowHF ((:&:) * f p)

RemA ((:&:) * f p) f

DistAnn s p s' => DistAnn ((:+:) * f s) p ((:+:) * ((:&:) * f p) s')

RemA s s' => RemA ((:+:) * ((:&:) * f p) s) ((:+:) * f s')

class DistAnn s p s' | s' -> s, s' -> p where

This class defines how to distribute an annotation over a sum of signatures.

Methods

injectA :: p -> s a :-> s' a

This function injects an annotation over a signature.

projectA :: s' a :-> (s a :&: p)

Instances

DistAnn f p ((:&:) * f p)

DistAnn s p s' => DistAnn ((:+:) * f s) p ((:+:) * ((:&:) * f p) s')

class RemA s s' | s -> s' where

Methods

remA :: s a :-> s' a

Instances

RemA ((:&:) * f p) f

RemA s s' => RemA ((:+:) * ((:&:) * f p) s) ((:+:) * f s')