Control.Category.Free

Free category

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

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)

complexity of foldNatFree2: O(n) where n is number of transitions embeded in Cat.

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)

complexity of composition (.): O(1) (worst case)

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)

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)

Defined in Control.Category.Free

Methods

zeroArrow :: Cat f b c

ArrowChoice f => ArrowChoice (Cat f)

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)

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)

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)

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)

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

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

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

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

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)

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)

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)

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)

Defined in Control.Category.Free

Methods

zeroArrow :: C f b c

ArrowChoice f => ArrowChoice (C f)

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)

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)

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)

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)

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

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

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

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

Oposite category

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

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)

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)

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)

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)

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)

complexity of foldNatFree2: O(n) where n is number of transitions embeded in Cat.

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)

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)

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

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

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