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

GetEmbD (Found p) f g => GetEmbD (Found (GoRight p)) f ((:+:) g' g)

GetEmbD (Found p) f g => GetEmbD (Found (GoLeft p)) f ((:+:) g g')

(GetEmbD (Found p1) f1 g, GetEmbD (Found p2) f2 g) => GetEmbD (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

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

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

(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

GoLeft Pos

GoRight Pos

Sum Pos Pos

data Emb

Constructors

NotFound

Ambiguous

Found Pos

type family GetEmb f g :: Emb

Equations

GetEmb f f = Found Here

GetEmb f (g1 :+: g2) = Pick f (g1 :+: g2) (GetEmb f g1) (GetEmb f g2)

GetEmb f g = NotFound

type family Pick f g e1 r :: Emb

Equations

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

Pick f g Ambiguous y = Ambiguous

Pick f g x Ambiguous = Ambiguous

Pick f g (Found x) y = Found (GoLeft x)

Pick f g x (Found y) = Found (GoRight y)

Pick f g x y = Split f g

type family Split f g :: Emb

Equations

Split (f1 :+: f2) g = Pick2 (GetEmb f1 g) (GetEmb f2 g)

Split f g = NotFound

type family Pick2 e1 r :: Emb

Equations

Pick2 (Found x) (Found y) = Found (Sum x y)

Pick2 Ambiguous y = Ambiguous

Pick2 x Ambiguous = Ambiguous

Pick2 NotFound y = NotFound

Pick2 x NotFound = NotFound

data EmbD e f g where

Constructors

HereD :: EmbD (Found Here) f f

GoLeftD :: EmbD (Found p) f g -> EmbD (Found (GoLeft p)) f (g :+: g')

GoRightD :: EmbD (Found p) f g -> EmbD (Found (GoRight p)) f (g' :+: g)

SumD :: EmbD (Found p1) f1 g -> EmbD (Found p2) f2 g -> EmbD (Found (Sum p1 p2)) (f1 :+: f2) g

class GetEmbD e f g where

Methods

getEmbD :: EmbD e f g

Instances

GetEmbD (Found Here) f f

GetEmbD (Found p) f g => GetEmbD (Found (GoRight p)) f ((:+:) g' g)

GetEmbD (Found p) f g => GetEmbD (Found (GoLeft p)) f ((:+:) g g')

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

data SimpPos

Constructors

SimpHere

SimpLeft SimpPos

SimpRight SimpPos

data Res

Constructors

CompPos SimpPos Pos

SingPos SimpPos

type family DestrPos e :: Res

Equations

DestrPos (GoLeft e) = ResLeft (DestrPos e)

DestrPos (GoRight e) = ResRight (DestrPos e)

DestrPos (Sum e1 e2) = ResSum (DestrPos e1) e2

DestrPos Here = SingPos SimpHere

type family ResLeft r :: Res

Equations

ResLeft (CompPos p e) = CompPos (SimpLeft p) (GoLeft e)

ResLeft (SingPos p) = SingPos (SimpLeft p)

type family ResRight r :: Res

Equations

ResRight (CompPos p e) = CompPos (SimpRight p) (GoRight e)

ResRight (SingPos p) = SingPos (SimpRight p)

type family ResSum r e :: Res

Equations

ResSum (CompPos p e1) e2 = CompPos p (Sum e1 e2)

ResSum (SingPos p) e = CompPos p e

type family Or x y

Equations

Or x False = x

Or False y = y

Or x y = True

type family In p e :: Bool

Equations

In SimpHere e = True

In p Here = True

In (SimpLeft p) (GoLeft e) = In p e

In (SimpRight p) (GoRight e) = In p e

In p (Sum e1 e2) = Or (In p e1) (In p e2)

In p e = False

type family Duplicates' r :: Bool

Equations

Duplicates' (SingPos p) = False

Duplicates' (CompPos p e) = Or (In p e) (Duplicates' (DestrPos e))

type family Duplicates e

Equations

Duplicates (Found p) = Duplicates' (DestrPos p)

class NoDup b f g

Instances

NoDup False f g

inj_ :: EmbD e f g -> f a -> g a

type (:<:) f g = (GetEmbD (GetEmb f g) f g, NoDup (Duplicates (GetEmb f g)) 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

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

proj_ :: EmbD e f g -> g a -> Maybe (f a)

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

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

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)

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

Inject an annotation over a signature.

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

Project an annotation from a signature.

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

Remove annotations from a signature.

Instances

RemA ((:&:) f p) f

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