free-category-0.0.4.0: Free category

Safe HaskellNone
LanguageHaskell2010
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

Synopsis

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 #

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 #

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

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 m is a monad on some subcategory of graphs (types of kind k -> 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