Data.Comp.Ops

This module provides operators on functors.

Documentation

data (f :+: g) e infixr 6

Formal sum of signatures (functors).

Constructors

Inl (f e)

Inr (g e)

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')

Subsume (Found p) f g => Subsume (Found (Ri p)) f ((:+:) * g' g)

Subsume (Found p) f g => Subsume (Found (Le p)) f ((:+:) * g g')

(Subsume (Found p1) f1 g, Subsume (Found p2) f2 g) => Subsume (Found (Sum p1 p2)) ((:+:) * f1 f2) g

(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)

fromInl :: (f :+: g) e -> Maybe (f e)

fromInr :: (f :+: g) e -> Maybe (g e)

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

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

data Pos

Constructors

Here

Le Pos

Ri Pos

Sum Pos Pos

data Emb

Constructors

Found Pos

NotFound

Ambiguous

type family Elem f g :: Emb

Equations

Elem f f = Found Here

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

Elem f g = NotFound

type family Choose f g e1 r :: Emb

Equations

Choose f g (Found x) (Found y) = Ambiguous

Choose f g Ambiguous y = Ambiguous

Choose f g x Ambiguous = Ambiguous

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

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

Choose (f1 :+: f2) g x y = Sum' (Elem f1 g) (Elem f2 g)

Choose f g 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 -> g a -> Maybe (f a)

Instances

Subsume (Found Here) f f

Subsume (Found p) f g => Subsume (Found (Ri p)) f ((:+:) * g' g)

Subsume (Found p) f g => Subsume (Found (Le p)) f ((:+:) * g g')

(Subsume (Found p1) f1 g, Subsume (Found p2) f2 g) => Subsume (Found (Sum p1 p2)) ((:+:) * f1 f2) g

type family Or a b :: Bool

Equations

Or False False = False

Or a b = True

type family AnyDupl f g

Equations

AnyDupl f f = False

AnyDupl f g = Or (Dupl f []) (Dupl g [])

type family Dupl f l :: Bool

Equations

Dupl (f :+: g) l = Dupl f (g : l)

Dupl f l = Or (Find f l) (Dupl' l)

type family Dupl' l :: Bool

Equations

Dupl' (f : l) = Or (Dupl f l) (Dupl' l)

Dupl' [] = False

type family Find f l :: Bool

Equations

Find f (g : l) = Or (Find' f g) (Find f l)

Find f [] = False

type family Find' f g :: Bool

Equations

Find' f (g1 :+: g2) = Or (Find' f g1) (Find' f g2)

Find' f f = True

Find' f g = False

class NoDupl f g s

Instances

NoDupl k k Bool f g False

type (:<:) f g = (Subsume (Elem f g) f g, NoDupl f g (AnyDupl f g)) infixl 5

The :<: constraint is a conjunction of two constraints. The first one is used to construct the evidence that is used to implement the injection and projection functions. The first constraint alone would allow instances such as F :+: F :<: F or F :+: (F :+: G) :<: F :+: G which have multiple occurrences of the same sub-signature on the left-hand side. Such instances are usually unintended and yield injection functions that are not injective. The second constraint excludes such instances.

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

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

Formal product of signatures (functors).

Constructors

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

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

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

data (f :&: a) e infixr 7

This data type adds a constant product (annotation) to a signature.

Constructors

(f e) :&: a infixr 7

Instances

DistAnn k f p ((:&:) k f p)

RemA k ((:&:) k f p) f

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 ((:&:) * f a)

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

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

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

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

(ArbitraryF f, Arbitrary p) => ArbitraryF ((:&:) * f p)

(NFDataF f, NFData a) => NFDataF ((:&:) * f a)

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

Inject an annotation over a signature.

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

Project an annotation from a signature.

Instances

DistAnn k f p ((:&:) k f p)

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

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

Methods

remA :: s a -> s' a

Remove annotations from a signature.

Instances

RemA k ((:&:) k f p) f

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