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

Control.Category.Free

Contents

Free category
Free category (CPS style)
Oposite category
Free interface re-exports

Synopsis

data Cat (f :: k -> k -> *) a b where
- Id :: Cat f a a
arrCat :: forall (f :: k -> k -> *) a b. f a b -> Cat f a b
mapCat :: forall (f :: k -> k -> *) a b c. f b c -> Cat f a b -> Cat f a c
foldCat :: forall f c a b. Category c => (forall x y. f x y -> c x y) -> Cat f a b -> c a b
newtype C f a b = C {
- runC :: forall r. Category r => (forall x y. f x y -> r x y) -> r 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
}
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
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

Free category

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

Efficient encoding of a category for which morphism composition has O(1) complexity and fold is linear in the number of transitions.

Constructors

Id :: Cat f a a

Instances

FreeAlgebra2 (Cat :: (k -> k -> Type) -> k -> k -> Type) Source #	complexity of `foldNatFree2`: `O(n)` where `n` is number of transitions embeded in `Cat`.
Instance details Defined in Control.Category.Free Methods liftFree2 :: AlgebraType0 Cat f => f a b -> Cat f a b # foldNatFree2 :: (AlgebraType Cat d, AlgebraType0 Cat f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> Cat f a b -> d a b # codom2 :: AlgebraType0 Cat f => Proof (AlgebraType Cat (Cat f)) (Cat f) # forget2 :: AlgebraType Cat f => Proof (AlgebraType0 Cat f) (Cat f) #
Category (Cat f :: k -> k -> Type) Source #	complexity of composition `(.)`: `O(1)` (worst case)
Instance details Defined in Control.Category.Free Methods id :: Cat f a a # (.) :: Cat f b c -> Cat f a b -> Cat f a c #
Arrow f => Arrow (Cat f) Source #
Instance details Defined in Control.Category.Free Methods arr :: (b -> c) -> Cat f b c # first :: Cat f b c -> Cat f (b, d) (c, d) # second :: Cat f b c -> Cat f (d, b) (d, c) # (***) :: Cat f b c -> Cat f b' c' -> Cat f (b, b') (c, c') # (&&&) :: Cat f b c -> Cat f b c' -> Cat f b (c, c') #
ArrowZero f => ArrowZero (Cat f) Source #
Instance details Defined in Control.Category.Free Methods zeroArrow :: Cat f b c #
ArrowChoice f => ArrowChoice (Cat f) Source #
Instance details Defined in Control.Category.Free Methods left :: Cat f b c -> Cat f (Either b d) (Either c d) # right :: Cat f b c -> Cat f (Either d b) (Either d c) # (+++) :: Cat f b c -> Cat f b' c' -> Cat f (Either b b') (Either c c') # (\|\|\|) :: Cat f b d -> Cat f c d -> Cat f (Either b c) d #
Semigroup (Cat f o o) Source #
Instance details Defined in Control.Category.Free Methods (<>) :: Cat f o o -> Cat f o o -> Cat f o o # sconcat :: NonEmpty (Cat f o o) -> Cat f o o # stimes :: Integral b => b -> Cat f o o -> Cat f o o #
Monoid (Cat f o o) Source #
Instance details Defined in Control.Category.Free Methods mempty :: Cat f o o # mappend :: Cat f o o -> Cat f o o -> Cat f o o # mconcat :: [Cat f o o] -> Cat f o o #
type AlgebraType0 (Cat :: (k -> k -> Type) -> k -> k -> Type) (f :: l) Source #
Instance details Defined in Control.Category.Free type AlgebraType0 (Cat :: (k -> k -> Type) -> k -> k -> Type) (f :: l) = ()
type AlgebraType (Cat :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) Source #
Instance details Defined in Control.Category.Free type AlgebraType (Cat :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) = Category c

arrCat :: forall (f :: k -> k -> *) a b. f a b -> Cat f a b Source #

Smart constructor for embeding spanning transitions into Cat, the same as liftFree2 @Cat. It is like arr for Arrows.

mapCat :: forall (f :: k -> k -> *) a b c. f b c -> Cat f a b -> Cat f a c Source #

Smart constructor mapCat for morphisms of Cat f category.

foldCat :: forall f c a b. Category c => (forall x y. f x y -> c x y) -> Cat f a b -> c a b Source #

Right fold of Cat into a category, the same as foldNatFree2 @Cat.

complexity: O(n) where n@ is number of transition embedded in Cat.

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 #
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

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

Isomorphism from Cat 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 specialisatin of hoistFreeH2.

Oposite 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 #
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 #

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.

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.

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 (Cat :: (k -> k -> Type) -> k -> k -> Type) Source #	complexity of `foldNatFree2`: `O(n)` where `n` is number of transitions embeded in `Cat`.
Instance details Defined in Control.Category.Free Methods liftFree2 :: AlgebraType0 Cat f => f a b -> Cat f a b # foldNatFree2 :: (AlgebraType Cat d, AlgebraType0 Cat f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> Cat f a b -> d a b # codom2 :: AlgebraType0 Cat f => Proof (AlgebraType Cat (Cat f)) (Cat f) # forget2 :: AlgebraType Cat f => Proof (AlgebraType0 Cat f) (Cat 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 (FreeEffCat m :: (k -> k -> Type) -> k -> k -> Type) Source #
Instance details Defined in Control.Category.FreeEff Methods liftFree2 :: AlgebraType0 (FreeEffCat m) f => f a b -> FreeEffCat m f a b # foldNatFree2 :: (AlgebraType (FreeEffCat m) d, AlgebraType0 (FreeEffCat m) f) => (forall (x :: k0) (y :: k0). f x y -> d x y) -> FreeEffCat m f a b -> d a b # codom2 :: AlgebraType0 (FreeEffCat m) f => Proof (AlgebraType (FreeEffCat m) (FreeEffCat m f)) (FreeEffCat m f) # forget2 :: AlgebraType (FreeEffCat m) f => Proof (AlgebraType0 (FreeEffCat m) f) (FreeEffCat 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 #

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

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

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

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 (typed of kind k -> k -> Type).