Copyright	(C) 2017-18 Jakub Daniel
License	BSD-style (see the file LICENSE)
Maintainer	Jakub Daniel <jakub.daniel@protonmail.com>
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Data.Expression.Utils.Indexed.Sum

Description

Synopsis

data (f :+: g) a i
- = InL (f a i)
- | InR (g a i)
class (IFunctor f, IFunctor g) => f :<: g where
- inj :: f a i -> g a i
- prj :: g a i -> Maybe (f a i)
class (IFunctor f, IFunctor g) => f :<<: g
inject :: g :<: f => forall i. g (IFix f) i -> IFix f i
match :: g :<: f => forall i. IFix f i -> Maybe (g (IFix f) i)
embed :: (IFunctor f, f :<<: g) => IFix f i -> IFix g i
restrict :: (ITraversable g, f :<<: g) => IFix g i -> Maybe (IFix f i)

Documentation

data (f :+: g) a i infixr 8 Source #

Sum of two indexed functors

Constructors

InL (f a i)
InR (g a i)

Instances

(IShow f, IShow g) => IShow (f :+: g :: (k1 -> Type) -> k2 -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods ishow :: (f :+: g) (Const String) i -> Const String i Source #
(IFunctor f, IFunctor g, IFunctor h, f :<<: g) => (f :: (k -> Type) -> k -> Type) :<<: (h :+: g :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods emb :: f a i -> (h :+: g) a i res :: (h :+: g) a i -> Maybe (f a i)
(IFunctor f, IFunctor g) => (f :: (k -> Type) -> k -> Type) :<<: (g :+: f :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods emb :: f a i -> (g :+: f) a i res :: (g :+: f) a i -> Maybe (f a i)
(IFunctor f, IFunctor g, IFunctor h, f :<: g) => (f :: (k -> Type) -> k -> Type) :<: (h :+: g :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods inj :: f a i -> (h :+: g) a i Source # prj :: (h :+: g) a i -> Maybe (f a i) Source #
(IFunctor f, IFunctor g) => (f :: (k -> Type) -> k -> Type) :<: (f :+: g :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods inj :: f a i -> (f :+: g) a i Source # prj :: (f :+: g) a i -> Maybe (f a i) Source #
(IEq1 f, IEq1 g) => IEq1 (f :+: g :: (i -> Type) -> i -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods ieq1 :: IEq a => (f :+: g) a j -> (f :+: g) a j -> Bool Source #
(IFoldable f, IFoldable g) => IFoldable (f :+: g :: (i -> Type) -> i -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods ifold :: Monoid m => (f :+: g) (Const m) i' -> Const m i' Source #
(IFunctor f, IFunctor g) => IFunctor (f :+: g :: (i -> Type) -> i -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods imap :: (forall (i' :: i0). a i' -> b i') -> forall (i' :: i0). (f :+: g) a i' -> (f :+: g) b i' Source # index :: (f :+: g) a i' -> Sing i' Source #
(ITraversable f, ITraversable g) => ITraversable (f :+: g :: (i -> Type) -> i -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods itraverse :: Applicative f0 => (forall (i' :: i0). a i' -> f0 (b i')) -> forall (i' :: i0). (f :+: g) a i' -> f0 ((f :+: g) b i') Source #
(MaybeQuantified f, MaybeQuantified g) => MaybeQuantified (f :+: g :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression Methods isQuantified' :: MaybeQuantified g0 => (f :+: g) (IFix g0) s -> Const Any s freevars' :: (f :+: g) (Const [DynamicallySorted Var]) s -> Const [DynamicallySorted Var] s
Heyting (ALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (==>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # neg :: ALia BooleanSort -> ALia BooleanSort # (<=>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
Heyting (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (==>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # neg :: QFALia BooleanSort -> QFALia BooleanSort # (<=>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
Heyting (Lia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (==>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # neg :: Lia BooleanSort -> Lia BooleanSort # (<=>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
Heyting (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (==>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # neg :: QFLia BooleanSort -> QFLia BooleanSort # (<=>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
Heyting (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods (==>) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # neg :: QFLogic BooleanSort -> QFLogic BooleanSort # (<=>) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
Lattice (ALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # (/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
Lattice (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # (/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
Lattice (Lia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # (/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
Lattice (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # (/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
Lattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # (/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
BoundedJoinSemiLattice (ALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods bottom :: ALia BooleanSort #
BoundedJoinSemiLattice (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods bottom :: QFALia BooleanSort #
BoundedJoinSemiLattice (Lia BooleanSort) Source #
Instance details Defined in Data.Expression Methods bottom :: Lia BooleanSort #
BoundedJoinSemiLattice (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression Methods bottom :: QFLia BooleanSort #
BoundedJoinSemiLattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods bottom :: QFLogic BooleanSort #
BoundedMeetSemiLattice (ALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods top :: ALia BooleanSort #
BoundedMeetSemiLattice (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods top :: QFALia BooleanSort #
BoundedMeetSemiLattice (Lia BooleanSort) Source #
Instance details Defined in Data.Expression Methods top :: Lia BooleanSort #
BoundedMeetSemiLattice (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression Methods top :: QFLia BooleanSort #
BoundedMeetSemiLattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods top :: QFLogic BooleanSort #
(Parseable f h, Parseable g h) => Parseable (f :+: g :: k1 -> k2 -> Type) h Source #
Instance details Defined in Data.Expression.Parser Methods parser :: Proxy (f :+: g) -> Parser (DynamicallySortedFix h) -> Parser (DynamicallySortedFix h) Source #

class (IFunctor f, IFunctor g) => f :<: g where Source #

Inclusion relation for indexed sum functors

Methods

inj :: f a i -> g a i Source #

prj :: g a i -> Maybe (f a i) Source #

Instances

IFunctor f => (f :: (i -> Type) -> i -> Type) :<: (f :: (i -> Type) -> i -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods inj :: f a i0 -> f a i0 Source # prj :: f a i0 -> Maybe (f a i0) Source #
(IFunctor f, IFunctor g, IFunctor h, f :<: g) => (f :: (k -> Type) -> k -> Type) :<: (h :+: g :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods inj :: f a i -> (h :+: g) a i Source # prj :: (h :+: g) a i -> Maybe (f a i) Source #
(IFunctor f, IFunctor g) => (f :: (k -> Type) -> k -> Type) :<: (f :+: g :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods inj :: f a i -> (f :+: g) a i Source # prj :: (f :+: g) a i -> Maybe (f a i) Source #

class (IFunctor f, IFunctor g) => f :<<: g Source #

Minimal complete definition

emb, res

Instances

(IFunctor f, IFunctor g, IFunctor h, f :<<: g) => (f :: (k -> Type) -> k -> Type) :<<: (h :+: g :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods emb :: f a i -> (h :+: g) a i res :: (h :+: g) a i -> Maybe (f a i)
(IFunctor f, IFunctor g) => (f :: (k -> Type) -> k -> Type) :<<: (g :+: f :: (k -> Type) -> k -> Type) Source #
Instance details Defined in Data.Expression.Utils.Indexed.Sum Methods emb :: f a i -> (g :+: f) a i res :: (g :+: f) a i -> Maybe (f a i)

inject :: g :<: f => forall i. g (IFix f) i -> IFix f i Source #

Inject a component into a sum.

match :: g :<: f => forall i. IFix f i -> Maybe (g (IFix f) i) Source #

Try to unpack a sum into a component.

embed :: (IFunctor f, f :<<: g) => IFix f i -> IFix g i Source #

Embed a subset in a superset.

restrict :: (ITraversable g, f :<<: g) => IFix g i -> Maybe (IFix f i) Source #

Try to restrict a superset to a subset.