Control.Category.Free

Real time Queue

data Queue (f :: k -> k -> Type) (a :: k) (b :: k) where

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)

Defined in Control.Category.Free.Internal

Methods

liftFree2 :: forall f (a :: k0) (b :: k0). AlgebraType0 Queue f => f a b -> Queue f a b

foldNatFree2 :: forall d f (a :: k0) (b :: k0). (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 :: forall (f :: k0 -> k0 -> Type). AlgebraType0 Queue f => Proof (AlgebraType Queue (Queue f)) (Queue f)

forget2 :: forall (f :: k0 -> k0 -> Type). AlgebraType Queue f => Proof (AlgebraType0 Queue f) (Queue f)

Category (Queue f :: k -> k -> Type)

Defined in Control.Category.Free.Internal

Methods

id :: forall (a :: k0). Queue f a a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). Queue f b c -> Queue f a b -> Queue f a c

Arrow f => Arrow (Queue f)

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)

Defined in Control.Category.Free.Internal

Methods

zeroArrow :: Queue f b c

ArrowChoice f => ArrowChoice (Queue f)

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)

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)

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)

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)

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)

Defined in Control.Category.Free.Internal

type AlgebraType (Queue :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) = Category c

consQ :: forall k (f :: k -> k -> Type) a b c. f b c -> Queue f a b -> Queue f a c

snocQ :: forall k (f :: k -> k -> Type) a b c. Queue f b c -> f a b -> Queue f a c

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

uncons a Queue, complexity: O(1)

liftQ :: forall k (f :: k -> k -> Type) a b. f a b -> Queue f a b

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

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

complexity O(n)

foldrQ :: forall k (f :: k -> k -> Type) 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

foldr of a Queue

foldlQ :: forall k (f :: k -> k -> Type) 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

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

Type alligned list

data ListTr :: (k -> k -> Type) -> k -> k -> Type where

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)

Defined in Control.Category.Free.Internal

Methods

liftFree2 :: forall f (a :: k0) (b :: k0). AlgebraType0 ListTr f => f a b -> ListTr f a b

foldNatFree2 :: forall d f (a :: k0) (b :: k0). (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 :: forall (f :: k0 -> k0 -> Type). AlgebraType0 ListTr f => Proof (AlgebraType ListTr (ListTr f)) (ListTr f)

forget2 :: forall (f :: k0 -> k0 -> Type). AlgebraType ListTr f => Proof (AlgebraType0 ListTr f) (ListTr f)

Category (ListTr f :: k -> k -> Type)

Defined in Control.Category.Free.Internal

Methods

id :: forall (a :: k0). ListTr f a a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). ListTr f b c -> ListTr f a b -> ListTr f a c

Arrow f => Arrow (ListTr f)

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)

Defined in Control.Category.Free.Internal

Methods

zeroArrow :: ListTr f b c

ArrowChoice f => ArrowChoice (ListTr f)

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)

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)

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)

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)

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)

Defined in Control.Category.Free.Internal

type AlgebraType (ListTr :: (k2 -> k2 -> Type) -> k2 -> k2 -> Type) (c :: k1 -> k1 -> Type) = Category c

liftL :: forall k (f :: k -> k -> Type) x y. f x y -> ListTr f x y

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

foldlL :: forall k (f :: k -> k -> Type) 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

foldl of a ListTr

TODO: make it strict, like foldl'.

foldrL :: forall k (f :: k -> k -> Type) 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

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

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 :: forall f (a :: k0) (b :: k0). AlgebraType0 C f => f a b -> C f a b

foldNatFree2 :: forall d f (a :: k0) (b :: k0). (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 :: forall (f :: k0 -> k0 -> Type). AlgebraType0 C f => Proof (AlgebraType C (C f)) (C f)

forget2 :: forall (f :: k0 -> k0 -> Type). AlgebraType C f => Proof (AlgebraType0 C f) (C f)

Category (C f :: k -> k -> Type)

Defined in Control.Category.Free

Methods

id :: forall (a :: k0). C f a a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). 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

(forall (x :: k) (y :: k). Show (f x y)) => Show (C f a b)

Show instance via ListTr

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)

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

liftC :: forall k (f :: k -> k -> Type) a b. f a b -> C f a b

consC :: forall k (f :: k -> k -> Type) a b c. f b c -> C f a b -> C f a c

foldNatC :: forall k (f :: k -> k -> Type) 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

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

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

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

Opposite category

newtype Op (f :: k -> k -> Type) (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 :: forall (a :: k0). Op f a a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). Op f b c -> Op f a b -> Op f a c

Show (f b a) => Show (Op f a b)

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)

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

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

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 :: forall f (a :: k) (b :: k). 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 :: forall d f (a :: k) (b :: k). (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 :: forall (f :: k -> k -> Type). 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 :: forall (f :: k -> k -> Type). 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 :: forall f (a :: k0) (b :: k0). AlgebraType0 ListTr f => f a b -> ListTr f a b

foldNatFree2 :: forall d f (a :: k0) (b :: k0). (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 :: forall (f :: k0 -> k0 -> Type). AlgebraType0 ListTr f => Proof (AlgebraType ListTr (ListTr f)) (ListTr f)

forget2 :: forall (f :: k0 -> k0 -> Type). AlgebraType ListTr f => Proof (AlgebraType0 ListTr f) (ListTr f)

FreeAlgebra2 (Queue :: (k -> k -> Type) -> k -> k -> Type)

Defined in Control.Category.Free.Internal

Methods

liftFree2 :: forall f (a :: k0) (b :: k0). AlgebraType0 Queue f => f a b -> Queue f a b

foldNatFree2 :: forall d f (a :: k0) (b :: k0). (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 :: forall (f :: k0 -> k0 -> Type). AlgebraType0 Queue f => Proof (AlgebraType Queue (Queue f)) (Queue f)

forget2 :: forall (f :: k0 -> k0 -> Type). AlgebraType Queue f => Proof (AlgebraType0 Queue f) (Queue f)

FreeAlgebra2 (C :: (k -> k -> Type) -> k -> k -> Type)

Defined in Control.Category.Free

Methods

liftFree2 :: forall f (a :: k0) (b :: k0). AlgebraType0 C f => f a b -> C f a b

foldNatFree2 :: forall d f (a :: k0) (b :: k0). (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 :: forall (f :: k0 -> k0 -> Type). AlgebraType0 C f => Proof (AlgebraType C (C f)) (C f)

forget2 :: forall (f :: k0 -> k0 -> Type). AlgebraType C f => Proof (AlgebraType0 C f) (C f)

Monad m => FreeAlgebra2 (EffCat m :: (k -> k -> Type) -> k -> k -> Type)

Defined in Control.Category.FreeEffect

Methods

liftFree2 :: forall f (a :: k0) (b :: k0). AlgebraType0 (EffCat m) f => f a b -> EffCat m f a b

foldNatFree2 :: forall d f (a :: k0) (b :: k0). (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 :: forall (f :: k0 -> k0 -> Type). AlgebraType0 (EffCat m) f => Proof (AlgebraType (EffCat m) (EffCat m f)) (EffCat m f)

forget2 :: forall (f :: k0 -> k0 -> Type). AlgebraType (EffCat m) f => Proof (AlgebraType0 (EffCat m) f) (EffCat m f)

FreeAlgebra2 A

Defined in Control.Arrow.Free

Methods

liftFree2 :: forall f (a :: k) (b :: k). AlgebraType0 A f => f a b -> A f a b

foldNatFree2 :: forall d f (a :: k) (b :: k). (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 :: forall (f :: k -> k -> Type). AlgebraType0 A f => Proof (AlgebraType A (A f)) (A f)

forget2 :: forall (f :: k -> k -> Type). AlgebraType A f => Proof (AlgebraType0 A f) (A f)

FreeAlgebra2 Arr

Defined in Control.Arrow.Free

Methods

liftFree2 :: forall f (a :: k) (b :: k). AlgebraType0 Arr f => f a b -> Arr f a b

foldNatFree2 :: forall d f (a :: k) (b :: k). (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 :: forall (f :: k -> k -> Type). AlgebraType0 Arr f => Proof (AlgebraType Arr (Arr f)) (Arr f)

forget2 :: forall (f :: k -> k -> Type). 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 :: forall k m f (a :: k) (b :: k). (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 :: forall k m f g (a :: k) (b :: k). (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 :: forall k m n (f :: k -> k -> Type) (a :: k) (b :: k). (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 :: forall k m (f :: k -> k -> Type) (a :: k) (b :: k). (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 :: forall k m f (g :: k -> k -> Type) (a :: k) (b :: k). (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