Safe Haskell	None
Language	Haskell2010
Extensions	Cpp MonoLocalBinds ScopedTypeVariables BangPatterns TypeFamilies ViewPatterns GADTs GADTSyntax PolyKinds InstanceSigs TypeSynonymInstances FlexibleContexts FlexibleInstances KindSignatures RankNTypes TypeOperators ExplicitNamespaces ExplicitForAll PatternSynonyms QuantifiedConstraints

Control.Category.Free

Contents

Real time Queue
Type alligned list
Free category (CPS style)
Opposite category
Free interface re-exports

Synopsis

data Queue (f :: k -> k -> *) (a :: k) (b :: k) where
- pattern ConsQ :: f b c -> Queue f a b -> Queue f a c
- pattern NilQ :: () => a ~ b => Queue f a b
consQ :: forall (f :: k -> k -> *) a b c. f b c -> Queue f a b -> Queue f a c
snocQ :: forall (f :: k -> k -> *) a b c. Queue f b c -> f a b -> Queue f a c
unconsQ :: Queue f a b -> ViewL f a b
liftQ :: forall (f :: k -> k -> *) a b. f a b -> Queue f a b
foldNatQ :: forall (f :: k -> k -> *) c a b. Category c => (forall x y. f x y -> c x y) -> Queue f a b -> c a b
foldrQ :: forall (f :: k -> k -> *) c a b d. (forall x y z. f y z -> c x y -> c x z) -> c a b -> Queue f b d -> c a d
foldlQ :: forall (f :: k -> k -> *) c a b d. (forall x y z. c y z -> f x y -> c x z) -> c b d -> Queue f a b -> c a d
zipWithQ :: forall f g a b a' b'. Category f => (forall x y x' y'. f x y -> f x' y' -> f (g x x') (g y y')) -> Queue f a b -> Queue f a' b' -> Queue f (g a a') (g b b')
data ListTr :: (k -> k -> *) -> k -> k -> * where
- NilTr :: ListTr f a a
- ConsTr :: f b c -> ListTr f a b -> ListTr f a c
liftL :: forall (f :: k -> k -> *) x y. f x y -> ListTr f x y
foldNatL :: forall (f :: k -> k -> *) c a b. Category c => (forall x y. f x y -> c x y) -> ListTr f a b -> c a b
foldlL :: forall (f :: k -> k -> *) c a b d. (forall x y z. c y z -> f x y -> c x z) -> c b d -> ListTr f a b -> c a d
foldrL :: forall (f :: k -> k -> *) c a b d. (forall x y z. f y z -> c x y -> c x z) -> c a b -> ListTr f b d -> c a d
zipWithL :: forall f g a b a' b'. Category f => (forall x y x' y'. f x y -> f x' y' -> f (g x x') (g y y')) -> ListTr f a b -> ListTr f a' b' -> ListTr f (g a a') (g b b')
newtype C f a b = C {
- runC :: forall r. Category r => (forall x y. f x y -> r x y) -> r a b
}
liftC :: forall (f :: k -> k -> *) a b. f a b -> C f a b
consC :: forall (f :: k -> k -> *) a b c. f b c -> C f a b -> C f a c
foldNatC :: forall (f :: k -> k -> *) c a b. Category c => (forall x y. f x y -> c x y) -> C f a b -> c a b
toC :: ListTr f a b -> C f a b
fromC :: C f a b -> ListTr f a b
newtype Op (f :: k -> k -> *) (a :: k) (b :: k) = Op {
- runOp :: f b a
}
hoistOp :: forall (f :: k -> k -> *) (g :: k -> k -> *) a b. (forall x y. f x y -> g x y) -> Op f a b -> Op g a b
class FreeAlgebra2 (m :: (k -> k -> Type) -> k -> k -> Type) where
- liftFree2 :: AlgebraType0 m f => f a b -> m f a b
- foldNatFree2 :: (AlgebraType m d, AlgebraType0 m f) => (forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
- codom2 :: AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)
- forget2 :: AlgebraType m f => Proof (AlgebraType0 m f) (m f)
wrapFree2 :: (AlgebraType0 m f, FreeAlgebra2 m, Monad (m f a)) => f a (m f a b) -> m f a b
foldFree2 :: (FreeAlgebra2 m, AlgebraType m f) => m f a b -> f a b
hoistFree2 :: (FreeAlgebra2 m, AlgebraType0 m g, AlgebraType0 m f) => (forall (x :: k) (y :: k). f x y -> g x y) -> m f a b -> m g a b
hoistFreeH2 :: (FreeAlgebra2 m, FreeAlgebra2 n, AlgebraType0 m f, AlgebraType0 n f, AlgebraType m (n f)) => m f a b -> n f a b
joinFree2 :: (FreeAlgebra2 m, AlgebraType0 m f) => m (m f) a b -> m f a b
bindFree2 :: (FreeAlgebra2 m, AlgebraType0 m g, AlgebraType0 m f) => m f a b -> (forall (x :: k) (y :: k). f x y -> m g x y) -> m g a b

Real time Queue

data Queue (f :: k -> k -> *) (a :: k) (b :: k) where Source #

Type alligned real time queues; Based on `Purely Functinal Data Structures` C.Okasaki. This the most reliably behaved implementation of free categories in this package.

Upper bounds of consQ, snocQ, unconsQ are O(1) (worst case).

Internal invariant: sum of lengths of two last least is equal the length of the first one.

Bundled Patterns

pattern ConsQ :: f b c -> Queue f a b -> Queue f a c
pattern NilQ :: () => a ~ b => Queue f a b

Instances

FreeAlgebra2 (Queue :: (k -> k -> Type) -> k -> k -> Type) Source #
Instance details Defined in Control.Category.Free.Internal Methods liftFree2 :: AlgebraType0 Queue f => f a b -> Queue f a b # foldNatFree2 :: (AlgebraType Queue d, AlgebraType0 Queue f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> Queue f a b -> d a b # codom2 :: AlgebraType0 Queue f => Proof (AlgebraType Queue (Queue f)) (Queue f) # forget2 :: AlgebraType Queue f => Proof (AlgebraType0 Queue f) (Queue f) #
Category (Queue f :: k -> k -> Type) Source #
Instance details Defined in Control.Category.Free.Internal Methods id :: Queue f a a # (.) :: Queue f b c -> Queue f a b -> Queue f a c #
Arrow f => Arrow (Queue f) Source #
Instance details Defined in Control.Category.Free.Internal Methods arr :: (b -> c) -> Queue f b c # first :: Queue f b c -> Queue f (b, d) (c, d) # second :: Queue f b c -> Queue f (d, b) (d, c) # (***) :: Queue f b c -> Queue f b' c' -> Queue f (b, b') (c, c') # (&&&) :: Queue f b c -> Queue f b c' -> Queue f b (c, c') #
ArrowZero f => ArrowZero (Queue f) Source #
Instance details Defined in Control.Category.Free.Internal Methods zeroArrow :: Queue f b c #
ArrowChoice f => ArrowChoice (Queue f) Source #
Instance details Defined in Control.Category.Free.Internal Methods left :: Queue f b c -> Queue f (Either b d) (Either c d) # right :: Queue f b c -> Queue f (Either d b) (Either d c) # (+++) :: Queue f b c -> Queue f b' c' -> Queue f (Either b b') (Either c c') # (\|\|\|) :: Queue f b d -> Queue f c d -> Queue f (Either b c) d #
(forall (x :: k) (y :: k). Show (f x y)) => Show (Queue f a b) Source #
Instance details Defined in Control.Category.Free.Internal Methods showsPrec :: Int -> Queue f a b -> ShowS # show :: Queue f a b -> String # showList :: [Queue f a b] -> ShowS #
Semigroup (Queue f o o) Source #
Instance details Defined in Control.Category.Free.Internal Methods (<>) :: Queue f o o -> Queue f o o -> Queue f o o # sconcat :: NonEmpty (Queue f o o) -> Queue f o o # stimes :: Integral b => b -> Queue f o o -> Queue f o o #
Monoid (Queue f o o) Source #
Instance details Defined in Control.Category.Free.Internal Methods mempty :: Queue f o o # mappend :: Queue f o o -> Queue f o o -> Queue f o o # mconcat :: [Queue f o o] -> Queue f o o #
type AlgebraType0 (Queue :: (k -> k -> Type) -> k -> k -> Type) (f :: l) Source #
Instance details Defined in Control.Category.Free.Internal type AlgebraType0 (Queue :: (k -> k -> Type) -> k -> k -> Type) (f :: l) = ()
type AlgebraType (Queue :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) Source #
Instance details Defined in Control.Category.Free.Internal type AlgebraType (Queue :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) = Category c

consQ :: forall (f :: k -> k -> *) a b c. f b c -> Queue f a b -> Queue f a c Source #

snocQ :: forall (f :: k -> k -> *) a b c. Queue f b c -> f a b -> Queue f a c Source #

unconsQ :: Queue f a b -> ViewL f a b Source #

uncons a Queue, complexity: O(1)

liftQ :: forall (f :: k -> k -> *) a b. f a b -> Queue f a b Source #

foldNatQ :: forall (f :: k -> k -> *) c a b. Category c => (forall x y. f x y -> c x y) -> Queue f a b -> c a b Source #

Efficient fold of a queue into a category, analogous to foldM.

complexity O(n)

foldrQ :: forall (f :: k -> k -> *) c a b d. (forall x y z. f y z -> c x y -> c x z) -> c a b -> Queue f b d -> c a d Source #

foldr of a Queue

foldlQ :: forall (f :: k -> k -> *) c a b d. (forall x y z. c y z -> f x y -> c x z) -> c b d -> Queue f a b -> c a d Source #

foldl of a Queue

TODO: make it strict, like foldl'.

zipWithQ :: forall f g a b a' b'. Category f => (forall x y x' y'. f x y -> f x' y' -> f (g x x') (g y y')) -> Queue f a b -> Queue f a' b' -> Queue f (g a a') (g b b') Source #

Type alligned list

data ListTr :: (k -> k -> *) -> k -> k -> * where Source #

Simple representation of a free category by using type aligned lists. This is not a surprise as free monoids can be represented by lists (up to laziness)

ListTr has FreeAlgebra2 class instance:

liftFree2    @ListTr :: f a b -> ListTr f ab
foldNatFree2 @ListTr :: Category d
                     => (forall x y. f x y -> d x y)
                     -> ListTr f a b
                     -> d a b

The same performance concerns that apply to Free apply to this encoding of a free category.

Note that even though this is a naive version, it behaves quite well in simple benchmarks and quite stable regardless of the level of optimisations.

Constructors

NilTr :: ListTr f a a
ConsTr :: f b c -> ListTr f a b -> ListTr f a c

Instances

FreeAlgebra2 (ListTr :: (k -> k -> Type) -> k -> k -> Type) Source #
Instance details Defined in Control.Category.Free.Internal Methods liftFree2 :: AlgebraType0 ListTr f => f a b -> ListTr f a b # foldNatFree2 :: (AlgebraType ListTr d, AlgebraType0 ListTr f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> ListTr f a b -> d a b # codom2 :: AlgebraType0 ListTr f => Proof (AlgebraType ListTr (ListTr f)) (ListTr f) # forget2 :: AlgebraType ListTr f => Proof (AlgebraType0 ListTr f) (ListTr f) #
Category (ListTr f :: k -> k -> Type) Source #
Instance details Defined in Control.Category.Free.Internal Methods id :: ListTr f a a # (.) :: ListTr f b c -> ListTr f a b -> ListTr f a c #
Arrow f => Arrow (ListTr f) Source #
Instance details Defined in Control.Category.Free.Internal Methods arr :: (b -> c) -> ListTr f b c # first :: ListTr f b c -> ListTr f (b, d) (c, d) # second :: ListTr f b c -> ListTr f (d, b) (d, c) # (***) :: ListTr f b c -> ListTr f b' c' -> ListTr f (b, b') (c, c') # (&&&) :: ListTr f b c -> ListTr f b c' -> ListTr f b (c, c') #
ArrowZero f => ArrowZero (ListTr f) Source #
Instance details Defined in Control.Category.Free.Internal Methods zeroArrow :: ListTr f b c #
ArrowChoice f => ArrowChoice (ListTr f) Source #
Instance details Defined in Control.Category.Free.Internal Methods left :: ListTr f b c -> ListTr f (Either b d) (Either c d) # right :: ListTr f b c -> ListTr f (Either d b) (Either d c) # (+++) :: ListTr f b c -> ListTr f b' c' -> ListTr f (Either b b') (Either c c') # (\|\|\|) :: ListTr f b d -> ListTr f c d -> ListTr f (Either b c) d #
(forall (x :: k) (y :: k). Show (f x y)) => Show (ListTr f a b) Source #
Instance details Defined in Control.Category.Free.Internal Methods showsPrec :: Int -> ListTr f a b -> ShowS # show :: ListTr f a b -> String # showList :: [ListTr f a b] -> ShowS #
Semigroup (ListTr f o o) Source #
Instance details Defined in Control.Category.Free.Internal Methods (<>) :: ListTr f o o -> ListTr f o o -> ListTr f o o # sconcat :: NonEmpty (ListTr f o o) -> ListTr f o o # stimes :: Integral b => b -> ListTr f o o -> ListTr f o o #
Monoid (ListTr f o o) Source #
Instance details Defined in Control.Category.Free.Internal Methods mempty :: ListTr f o o # mappend :: ListTr f o o -> ListTr f o o -> ListTr f o o # mconcat :: [ListTr f o o] -> ListTr f o o #
type AlgebraType0 (ListTr :: (k -> k -> Type) -> k -> k -> Type) (f :: l) Source #
Instance details Defined in Control.Category.Free.Internal type AlgebraType0 (ListTr :: (k -> k -> Type) -> k -> k -> Type) (f :: l) = ()
type AlgebraType (ListTr :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) Source #
Instance details Defined in Control.Category.Free.Internal type AlgebraType (ListTr :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) = Category c

liftL :: forall (f :: k -> k -> *) x y. f x y -> ListTr f x y Source #

foldNatL :: forall (f :: k -> k -> *) c a b. Category c => (forall x y. f x y -> c x y) -> ListTr f a b -> c a b Source #

foldlL :: forall (f :: k -> k -> *) c a b d. (forall x y z. c y z -> f x y -> c x z) -> c b d -> ListTr f a b -> c a d Source #

foldl of a ListTr

TODO: make it strict, like foldl'.

foldrL :: forall (f :: k -> k -> *) c a b d. (forall x y z. f y z -> c x y -> c x z) -> c a b -> ListTr f b d -> c a d Source #

foldr of a ListTr

zipWithL :: forall f g a b a' b'. Category f => (forall x y x' y'. f x y -> f x' y' -> f (g x x') (g y y')) -> ListTr f a b -> ListTr f a' b' -> ListTr f (g a a') (g b b') Source #

Free category (CPS style)

newtype C f a b Source #

CPS style encoded free category; one can use FreeAlgebra2 class instance:

liftFree2    @C :: f a b -> C f a b
foldNatFree2 @C :: Category d
                => (forall x y. f x y -> d x y)
                -> C f a b -> d a b

Constructors

C
Fields runC :: forall r. Category r => (forall x y. f x y -> r x y) -> r a b

Instances

FreeAlgebra2 (C :: (k -> k -> Type) -> k -> k -> Type) Source #
Instance details Defined in Control.Category.Free Methods liftFree2 :: AlgebraType0 C f => f a b -> C f a b # foldNatFree2 :: (AlgebraType C d, AlgebraType0 C f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> C f a b -> d a b # codom2 :: AlgebraType0 C f => Proof (AlgebraType C (C f)) (C f) # forget2 :: AlgebraType C f => Proof (AlgebraType0 C f) (C f) #
Category (C f :: k -> k -> Type) Source #
Instance details Defined in Control.Category.Free Methods id :: C f a a # (.) :: C f b c -> C f a b -> C f a c #
Arrow f => Arrow (C f) Source #
Instance details Defined in Control.Category.Free Methods arr :: (b -> c) -> C f b c # first :: C f b c -> C f (b, d) (c, d) # second :: C f b c -> C f (d, b) (d, c) # (***) :: C f b c -> C f b' c' -> C f (b, b') (c, c') # (&&&) :: C f b c -> C f b c' -> C f b (c, c') #
ArrowZero f => ArrowZero (C f) Source #
Instance details Defined in Control.Category.Free Methods zeroArrow :: C f b c #
ArrowChoice f => ArrowChoice (C f) Source #
Instance details Defined in Control.Category.Free Methods left :: C f b c -> C f (Either b d) (Either c d) # right :: C f b c -> C f (Either d b) (Either d c) # (+++) :: C f b c -> C f b' c' -> C f (Either b b') (Either c c') # (\|\|\|) :: C f b d -> C f c d -> C f (Either b c) d #
(forall (x :: k) (y :: k). Show (f x y)) => Show (C f a b) Source #	Show instance via `ListTr`
Instance details Defined in Control.Category.Free Methods showsPrec :: Int -> C f a b -> ShowS # show :: C f a b -> String # showList :: [C f a b] -> ShowS #
Semigroup (C f o o) Source #
Instance details Defined in Control.Category.Free Methods (<>) :: C f o o -> C f o o -> C f o o # sconcat :: NonEmpty (C f o o) -> C f o o # stimes :: Integral b => b -> C f o o -> C f o o #
Monoid (C f o o) Source #
Instance details Defined in Control.Category.Free Methods mempty :: C f o o # mappend :: C f o o -> C f o o -> C f o o # mconcat :: [C f o o] -> C f o o #
type AlgebraType0 (C :: (k -> k -> Type) -> k -> k -> Type) (f :: l) Source #
Instance details Defined in Control.Category.Free type AlgebraType0 (C :: (k -> k -> Type) -> k -> k -> Type) (f :: l) = ()
type AlgebraType (C :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) Source #
Instance details Defined in Control.Category.Free type AlgebraType (C :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) = Category c

liftC :: forall (f :: k -> k -> *) a b. f a b -> C f a b Source #

consC :: forall (f :: k -> k -> *) a b c. f b c -> C f a b -> C f a c Source #

foldNatC :: forall (f :: k -> k -> *) c a b. Category c => (forall x y. f x y -> c x y) -> C f a b -> c a b Source #

toC :: ListTr f a b -> C f a b Source #

Isomorphism from ListTr to C, which is a specialisation of hoistFreeH2.

fromC :: C f a b -> ListTr f a b Source #

Inverse of fromC, which also is a specialisation of hoistFreeH2.

Opposite category

newtype Op (f :: k -> k -> *) (a :: k) (b :: k) Source #

Oposite categoy in which arrows from a to b are represented by arrows from b to a in the original category.

Constructors

Op
Fields runOp :: f b a

Instances

Category f => Category (Op f :: k -> k -> Type) Source #
Instance details Defined in Control.Category.Free.Internal Methods id :: Op f a a # (.) :: Op f b c -> Op f a b -> Op f a c #
Show (f b a) => Show (Op f a b) Source #
Instance details Defined in Control.Category.Free.Internal Methods showsPrec :: Int -> Op f a b -> ShowS # show :: Op f a b -> String # showList :: [Op f a b] -> ShowS #
Category f => Semigroup (Op f o o) Source #
Instance details Defined in Control.Category.Free.Internal Methods (<>) :: Op f o o -> Op f o o -> Op f o o # sconcat :: NonEmpty (Op f o o) -> Op f o o # stimes :: Integral b => b -> Op f o o -> Op f o o #
Category f => Monoid (Op f o o) Source #
Instance details Defined in Control.Category.Free.Internal Methods mempty :: Op f o o # mappend :: Op f o o -> Op f o o -> Op f o o # mconcat :: [Op f o o] -> Op f o o #

hoistOp :: forall (f :: k -> k -> *) (g :: k -> k -> *) a b. (forall x y. f x y -> g x y) -> Op f a b -> Op g a b Source #

Op is an endo-functor of the category of categories.

Free interface re-exports

class FreeAlgebra2 (m :: (k -> k -> Type) -> k -> k -> Type) where #

Free algebra class similar to FreeAlgebra1 and FreeAlgebra, but for types of kind k -> k -> Type.

Minimal complete definition

liftFree2, foldNatFree2

Methods

liftFree2 :: AlgebraType0 m f => f a b -> m f a b #

Lift a graph f satsifying the constraint AlgebraType0 to a free its object m f.

foldNatFree2 :: (AlgebraType m d, AlgebraType0 m f) => (forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b #

This represents the theorem that m f is indeed free object (as in propositions as types). The types of kind k -> k -> Type form a category, where an arrow from f :: k -> k -> Type to d :: k -> k -> Type is represented by type forall x y. f x y -> d x y. foldNatFree2 states that whenever we have such a morphism and d satisfies the constraint AlgebraType m d then we can construct a morphism from m f to d.

foldNatFree2 nat (liftFree2 tr) = nat tr

foldNatFree2 nat . foldNatFree2 nat' = foldNatFree2 (foldNatFree2 nat . nat')

codom2 :: AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f) #

A proof that for each f satisfying AlgebraType0 m f, m f satisfies AlgebraType m (m f) constrant. This means that m is a well defined functor from the full sub-category of types of kind k -> k -> Type which satisfy the AlgebraType0 m constraint to the full subcategory of types of the same kind which satifsfy the constraint AlgebraType m.

forget2 :: AlgebraType m f => Proof (AlgebraType0 m f) (m f) #

A proof that each type f :: k -> k -> Type satisfying the Algebra m f constraint also satisfies AlgebraType0 m f. This states that there is a well defined forgetful functor from the category of types of kind k -> k -> Type which satisfy the AlgebraType m to the category of types of the same kind which satisfy the AlgebraType0 m constraint.

Instances

FreeAlgebra2 (ListTr :: (k -> k -> Type) -> k -> k -> Type) Source #
Instance details Defined in Control.Category.Free.Internal Methods liftFree2 :: AlgebraType0 ListTr f => f a b -> ListTr f a b # foldNatFree2 :: (AlgebraType ListTr d, AlgebraType0 ListTr f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> ListTr f a b -> d a b # codom2 :: AlgebraType0 ListTr f => Proof (AlgebraType ListTr (ListTr f)) (ListTr f) # forget2 :: AlgebraType ListTr f => Proof (AlgebraType0 ListTr f) (ListTr f) #
FreeAlgebra2 (Queue :: (k -> k -> Type) -> k -> k -> Type) Source #
Instance details Defined in Control.Category.Free.Internal Methods liftFree2 :: AlgebraType0 Queue f => f a b -> Queue f a b # foldNatFree2 :: (AlgebraType Queue d, AlgebraType0 Queue f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> Queue f a b -> d a b # codom2 :: AlgebraType0 Queue f => Proof (AlgebraType Queue (Queue f)) (Queue f) # forget2 :: AlgebraType Queue f => Proof (AlgebraType0 Queue f) (Queue f) #
FreeAlgebra2 (C :: (k -> k -> Type) -> k -> k -> Type) Source #
Instance details Defined in Control.Category.Free Methods liftFree2 :: AlgebraType0 C f => f a b -> C f a b # foldNatFree2 :: (AlgebraType C d, AlgebraType0 C f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> C f a b -> d a b # codom2 :: AlgebraType0 C f => Proof (AlgebraType C (C f)) (C f) # forget2 :: AlgebraType C f => Proof (AlgebraType0 C f) (C f) #
Monad m => FreeAlgebra2 (EffCat m :: (k -> k -> Type) -> k -> k -> Type) Source #
Instance details Defined in Control.Category.FreeEffect Methods liftFree2 :: AlgebraType0 (EffCat m) f => f a b -> EffCat m f a b # foldNatFree2 :: (AlgebraType (EffCat m) d, AlgebraType0 (EffCat m) f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> EffCat m f a b -> d a b # codom2 :: AlgebraType0 (EffCat m) f => Proof (AlgebraType (EffCat m) (EffCat m f)) (EffCat m f) # forget2 :: AlgebraType (EffCat m) f => Proof (AlgebraType0 (EffCat m) f) (EffCat m f) #
FreeAlgebra2 A Source #
Instance details Defined in Control.Arrow.Free Methods liftFree2 :: AlgebraType0 A f => f a b -> A f a b # foldNatFree2 :: (AlgebraType A d, AlgebraType0 A f) => (forall (x :: k) (y :: k). f x y -> d x y) -> A f a b -> d a b # codom2 :: AlgebraType0 A f => Proof (AlgebraType A (A f)) (A f) # forget2 :: AlgebraType A f => Proof (AlgebraType0 A f) (A f) #
FreeAlgebra2 Arr Source #
Instance details Defined in Control.Arrow.Free Methods liftFree2 :: AlgebraType0 Arr f => f a b -> Arr f a b # foldNatFree2 :: (AlgebraType Arr d, AlgebraType0 Arr f) => (forall (x :: k) (y :: k). f x y -> d x y) -> Arr f a b -> d a b # codom2 :: AlgebraType0 Arr f => Proof (AlgebraType Arr (Arr f)) (Arr f) # forget2 :: AlgebraType Arr f => Proof (AlgebraType0 Arr f) (Arr f) #

wrapFree2 :: (AlgebraType0 m f, FreeAlgebra2 m, Monad (m f a)) => f a (m f a b) -> m f a b #

Version of wrap from free package but for graphs.

foldFree2 :: (FreeAlgebra2 m, AlgebraType m f) => m f a b -> f a b #

Like foldFree or foldFree1 but for graphs.

A lawful instance will satisfy:

 foldFree2 . liftFree2 == id :: f a b -> f a b

It is the unit of adjuction defined by FreeAlgebra1 class.

hoistFree2 :: (FreeAlgebra2 m, AlgebraType0 m g, AlgebraType0 m f) => (forall (x :: k) (y :: k). f x y -> g x y) -> m f a b -> m g a b #

Hoist the underlying graph in the free structure. This is a higher version of a functor (analogous to fmapFree, which defined functor instance for FreeAlgebra instances) and it satisfies the functor laws:

hoistFree2 id = id

hoistFree2 f . hoistFree2 g = hoistFree2 (f . g)

hoistFreeH2 :: (FreeAlgebra2 m, FreeAlgebra2 n, AlgebraType0 m f, AlgebraType0 n f, AlgebraType m (n f)) => m f a b -> n f a b #

Hoist the top level free structure.

joinFree2 :: (FreeAlgebra2 m, AlgebraType0 m f) => m (m f) a b -> m f a b #

FreeAlgebra2 mis a monad on some subcategory of graphs (types of kindk -> k -> Type@), joinFree it is the join of this monad.

foldNatFree2 nat . joinFree2 = foldNatFree2 (foldNatFree2 nat)

This property is analogous to foldMap f . concat = foldMap (foldMap f),

bindFree2 :: (FreeAlgebra2 m, AlgebraType0 m g, AlgebraType0 m f) => m f a b -> (forall (x :: k) (y :: k). f x y -> m g x y) -> m g a b #

bind of the monad defined by m on the subcategory of graphs (types of kind k -> k -> Type).

foldNatFree2 nat (bindFree mf nat') = foldNatFree2 (foldNatFree2 nat . nat') mf