{-# LANGUAGE CPP                 #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE InstanceSigs        #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module Control.Arrow.Free
  ( -- * Free arrow
    Arr (Id, Arr, Prod)
  , arrArr
  , mapArr
  , foldArr

    -- * Free arrow (CPS style)
  , A (..)
  , fromA
  , toA
    -- * Free interface re-exports
  , FreeAlgebra2 (..)
  , wrapFree2
  , foldFree2
  , hoistFree2
  , joinFree2
  , bindFree2
  ) where

import           Prelude hiding (id, (.))
import           Control.Arrow (Arrow (..))
import           Control.Category (Category (..))
#if __GLASGOW_HASKELL__ < 804
import           Data.Monoid (Monoid (..))
import           Data.Semigroup (Semigroup (..))
#endif

import           Control.Algebra.Free2
  ( AlgebraType0
  , AlgebraType
  , FreeAlgebra2 (..)
  , Proof (..)
  , wrapFree2
  , foldFree2
  , hoistFree2
  , hoistFreeH2
  , joinFree2
  , bindFree2
  )
import           Control.Category.Free.Internal

data Arr f a b where
  Id    :: Arr f a a
  Cons  :: f b c     -> Queue (Arr f) a b -> Arr f a c
  Arr   :: (b -> c)  -> Arr f a b -> Arr f a c
  Prod  :: Arr f a b -> Arr f a c -> Arr f a (b, c)

arrArr :: (b -> c) -> Arr f b c
arrArr :: (b -> c) -> Arr f b c
arrArr b -> c
bc = (b -> c) -> Arr f b b -> Arr f b c
forall b c (f :: * -> * -> *) a. (b -> c) -> Arr f a b -> Arr f a c
Arr b -> c
bc Arr f b b
forall (f :: * -> * -> *) a. Arr f a a
Id

mapArr :: f b c
       -> Arr f a b
       -> Arr f a c
mapArr :: f b c -> Arr f a b -> Arr f a c
mapArr f b c
bc Arr f a b
ac = f b c -> Queue (Arr f) b b -> Arr f b c
forall (f :: * -> * -> *) b c a.
f b c -> Queue (Arr f) a b -> Arr f a c
Cons f b c
bc Queue (Arr f) b b
forall k (f :: k -> k -> *) (a :: k). Queue f a a
nilQ Arr f b c -> Arr f a b -> Arr f a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f a b
ac

foldArr :: forall f arr a b.
           Arrow arr
        => (forall x y. f x y -> arr x y)
        -> Arr f a b
        -> arr a b
foldArr :: (forall x y. f x y -> arr x y) -> Arr f a b -> arr a b
foldArr forall x y. f x y -> arr x y
_   Arr f a b
Id = arr a b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
foldArr forall x y. f x y -> arr x y
fun (Cons f b b
bc Queue (Arr f) a b
ab) = f b b -> arr b b
forall x y. f x y -> arr x y
fun f b b
bc arr b b -> arr a b -> arr a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall x y. Arr f x y -> arr x y) -> Queue (Arr f) a b -> arr a b
forall k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k).
Category c =>
(forall (x :: k) (y :: k). f x y -> c x y) -> Queue f a b -> c a b
foldNatQ ((forall x y. f x y -> arr x y) -> Arr f x y -> arr x y
forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall x y. f x y -> arr x y
fun) Queue (Arr f) a b
ab
foldArr forall x y. f x y -> arr x y
fun (Arr b -> b
f Arr f a b
g)    = (b -> b) -> arr b b
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> b
f  arr b b -> arr a b -> arr a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall x y. f x y -> arr x y) -> Arr f a b -> arr a b
forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall x y. f x y -> arr x y
fun Arr f a b
g
foldArr forall x y. f x y -> arr x y
fun (Prod Arr f a b
f Arr f a c
g)   = (forall x y. f x y -> arr x y) -> Arr f a b -> arr a b
forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall x y. f x y -> arr x y
fun Arr f a b
f arr a b -> arr a c -> arr a (b, c)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (forall x y. f x y -> arr x y) -> Arr f a c -> arr a c
forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall x y. f x y -> arr x y
fun Arr f a c
g

instance Category (Arr f) where
  id :: Arr f a a
id = Arr f a a
forall (f :: * -> * -> *) a. Arr f a a
Id
  Arr f b c
Id         . :: Arr f b c -> Arr f a b -> Arr f a c
. Arr f a b
f  = Arr f a b
Arr f a c
f
  Arr f b c
f          . Arr f a b
Id = Arr f b c
Arr f a c
f
  (Cons f b c
f Queue (Arr f) b b
g) . Arr f a b
h  = f b c -> Queue (Arr f) a b -> Arr f a c
forall (f :: * -> * -> *) b c a.
f b c -> Queue (Arr f) a b -> Arr f a c
Cons f b c
f (Queue (Arr f) b b
g Queue (Arr f) b b -> Arr f a b -> Queue (Arr f) a b
forall k (f :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Queue f b c -> f a b -> Queue f a c
`snocQ` Arr f a b
h)
  (Arr b -> c
f Arr f b b
g)  . Arr f a b
h  = (b -> c) -> Arr f a b -> Arr f a c
forall b c (f :: * -> * -> *) a. (b -> c) -> Arr f a b -> Arr f a c
Arr b -> c
f (Arr f b b
g Arr f b b -> Arr f a b -> Arr f a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f a b
h)
  (Prod Arr f b b
f Arr f b c
g) . Arr f a b
h  = Arr f a b -> Arr f a c -> Arr f a (b, c)
forall (f :: * -> * -> *) a b c.
Arr f a b -> Arr f a c -> Arr f a (b, c)
Prod (Arr f b b
f Arr f b b -> Arr f a b -> Arr f a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f a b
h) (Arr f b c
g Arr f b c -> Arr f a b -> Arr f a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f a b
h)

instance Semigroup (Arr f o o) where
    Arr f o o
f <> :: Arr f o o -> Arr f o o -> Arr f o o
<> Arr f o o
g = Arr f o o
f Arr f o o -> Arr f o o -> Arr f o o
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f o o
g

instance Monoid (Arr f o o) where
    mempty :: Arr f o o
mempty = Arr f o o
forall (f :: * -> * -> *) a. Arr f a a
Id
#if __GLASGOW_HASKELL__ < 804
    mappend = (<>)
#endif

instance Arrow (Arr f) where
  arr :: (b -> c) -> Arr f b c
arr       = (b -> c) -> Arr f b c
forall b c (f :: * -> * -> *). (b -> c) -> Arr f b c
arrArr
  first :: Arr f b c -> Arr f (b, d) (c, d)
first Arr f b c
bc  = Arr f (b, d) c -> Arr f (b, d) d -> Arr f (b, d) (c, d)
forall (f :: * -> * -> *) a b c.
Arr f a b -> Arr f a c -> Arr f a (b, c)
Prod (Arr f b c
bc Arr f b c -> Arr f (b, d) b -> Arr f (b, d) c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((b, d) -> b) -> Arr f (b, d) b
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (b, d) -> b
forall a b. (a, b) -> a
fst) (((b, d) -> d) -> Arr f (b, d) d
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (b, d) -> d
forall a b. (a, b) -> b
snd)
  second :: Arr f b c -> Arr f (d, b) (d, c)
second Arr f b c
bc = Arr f (d, b) d -> Arr f (d, b) c -> Arr f (d, b) (d, c)
forall (f :: * -> * -> *) a b c.
Arr f a b -> Arr f a c -> Arr f a (b, c)
Prod (((d, b) -> d) -> Arr f (d, b) d
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (d, b) -> d
forall a b. (a, b) -> a
fst) (Arr f b c
bc Arr f b c -> Arr f (d, b) b -> Arr f (d, b) c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((d, b) -> b) -> Arr f (d, b) b
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (d, b) -> b
forall a b. (a, b) -> b
snd)
  Arr f b c
ab *** :: Arr f b c -> Arr f b' c' -> Arr f (b, b') (c, c')
*** Arr f b' c'
xy = Arr f (b, b') c -> Arr f (b, b') c' -> Arr f (b, b') (c, c')
forall (f :: * -> * -> *) a b c.
Arr f a b -> Arr f a c -> Arr f a (b, c)
Prod (Arr f b c
ab Arr f b c -> Arr f (b, b') b -> Arr f (b, b') c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((b, b') -> b) -> Arr f (b, b') b
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (b, b') -> b
forall a b. (a, b) -> a
fst) (Arr f b' c'
xy Arr f b' c' -> Arr f (b, b') b' -> Arr f (b, b') c'
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((b, b') -> b') -> Arr f (b, b') b'
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (b, b') -> b'
forall a b. (a, b) -> b
snd)
  &&& :: Arr f b c -> Arr f b c' -> Arr f b (c, c')
(&&&)     = Arr f b c -> Arr f b c' -> Arr f b (c, c')
forall (f :: * -> * -> *) a b c.
Arr f a b -> Arr f a c -> Arr f a (b, c)
Prod

type instance AlgebraType0 Arr f = ()
type instance AlgebraType  Arr c = Arrow c

instance FreeAlgebra2 Arr where
  liftFree2 :: f a b -> Arr f a b
liftFree2 = \f a b
fab -> f a b -> Queue (Arr f) a a -> Arr f a b
forall (f :: * -> * -> *) b c a.
f b c -> Queue (Arr f) a b -> Arr f a c
Cons f a b
fab Queue (Arr f) a a
forall k (f :: k -> k -> *) (a :: k). Queue f a a
nilQ
  {-# INLINE liftFree2 #-}

  foldNatFree2 :: (forall x y. f x y -> d x y) -> Arr f a b -> d a b
foldNatFree2 = (forall x y. f x y -> d x y) -> Arr f a b -> d a b
forall (f :: * -> * -> *) (arr :: * -> * -> *) a b.
Arrow arr =>
(forall x y. f x y -> arr x y) -> Arr f a b -> arr a b
foldArr
  {-# INLINE foldNatFree2 #-}

  codom2 :: Proof (AlgebraType Arr (Arr f)) (Arr f)
codom2  = Proof (AlgebraType Arr (Arr f)) (Arr f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: Proof (AlgebraType0 Arr f) (Arr f)
forget2 = Proof (AlgebraType0 Arr f) (Arr f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof

--
-- Free arrows using CSP style
--

-- | Free arrow using CPS style.
--
newtype A f a b
  = A { A f a b
-> forall (r :: * -> * -> *).
   Arrow r =>
   (forall x y. f x y -> r x y) -> r a b
runA :: forall r. Arrow r
             => (forall x y. f x y -> r x y)
             -> r a b
      }

-- |
-- Isomorphism from @'Arr'@ to @'A'@, which is a specialisation of
-- @'hoistFreeH2'@.
toA :: Arr f a b -> A f a b
toA :: Arr f a b -> A f a b
toA = Arr f a b -> A f a b
forall k (m :: (k -> k -> *) -> k -> k -> *)
       (n :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *) (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
hoistFreeH2
{-# INLINE toA #-}

-- |
-- Inverse of @'fromA'@, which also is a specialisatin of @'hoistFreeH2'@.
fromA :: A f a b -> Arr f a b
fromA :: A f a b -> Arr f a b
fromA = A f a b -> Arr f a b
forall k (m :: (k -> k -> *) -> k -> k -> *)
       (n :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *) (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
hoistFreeH2
{-# INLINE fromA #-}

instance Category (A f) where
  id :: A f a a
id = (forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a a)
-> A f a a
forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A (\forall x y. f x y -> r x y
_ -> r a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
  A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f . :: A f b c -> A f a b -> A f a c
. A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r a b
g = (forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a c)
-> A f a c
forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A ((forall (r :: * -> * -> *).
  Arrow r =>
  (forall x y. f x y -> r x y) -> r a c)
 -> A f a c)
-> (forall (r :: * -> * -> *).
    Arrow r =>
    (forall x y. f x y -> r x y) -> r a c)
-> A f a c
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> (forall x y. f x y -> r x y) -> r b c
forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f forall x y. f x y -> r x y
k r b c -> r a b -> r a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall x y. f x y -> r x y) -> r a b
forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r a b
g forall x y. f x y -> r x y
k

instance Semigroup (A f o o) where
    A f o o
f <> :: A f o o -> A f o o -> A f o o
<> A f o o
g = A f o o
f A f o o -> A f o o -> A f o o
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. A f o o
g

instance Monoid (A f o o) where
    mempty :: A f o o
mempty = A f o o
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
#if __GLASGOW_HASKELL__ < 804
    mappend = (<>)
#endif

instance Arrow (A f) where
  arr :: (b -> c) -> A f b c
arr b -> c
f = (forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r b c)
-> A f b c
forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A (\forall x y. f x y -> r x y
_ -> ((b -> c) -> r b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
f))
  A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f *** :: A f b c -> A f b' c' -> A f (b, b') (c, c')
*** A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b' c'
g  = (forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r (b, b') (c, c'))
-> A f (b, b') (c, c')
forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A ((forall (r :: * -> * -> *).
  Arrow r =>
  (forall x y. f x y -> r x y) -> r (b, b') (c, c'))
 -> A f (b, b') (c, c'))
-> (forall (r :: * -> * -> *).
    Arrow r =>
    (forall x y. f x y -> r x y) -> r (b, b') (c, c'))
-> A f (b, b') (c, c')
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> (forall x y. f x y -> r x y) -> r b c
forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f forall x y. f x y -> r x y
k r b c -> r b' c' -> r (b, b') (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (forall x y. f x y -> r x y) -> r b' c'
forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b' c'
g forall x y. f x y -> r x y
k
  first :: A f b c -> A f (b, d) (c, d)
first  (A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f) = (forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r (b, d) (c, d))
-> A f (b, d) (c, d)
forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A ((forall (r :: * -> * -> *).
  Arrow r =>
  (forall x y. f x y -> r x y) -> r (b, d) (c, d))
 -> A f (b, d) (c, d))
-> (forall (r :: * -> * -> *).
    Arrow r =>
    (forall x y. f x y -> r x y) -> r (b, d) (c, d))
-> A f (b, d) (c, d)
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> r b c -> r (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((forall x y. f x y -> r x y) -> r b c
forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f forall x y. f x y -> r x y
k)
  second :: A f b c -> A f (d, b) (d, c)
second (A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f) = (forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r (d, b) (d, c))
-> A f (d, b) (d, c)
forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A ((forall (r :: * -> * -> *).
  Arrow r =>
  (forall x y. f x y -> r x y) -> r (d, b) (d, c))
 -> A f (d, b) (d, c))
-> (forall (r :: * -> * -> *).
    Arrow r =>
    (forall x y. f x y -> r x y) -> r (d, b) (d, c))
-> A f (d, b) (d, c)
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> r b c -> r (d, b) (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((forall x y. f x y -> r x y) -> r b c
forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f forall x y. f x y -> r x y
k)

type instance AlgebraType0 A f = ()
type instance AlgebraType  A c = Arrow c

instance FreeAlgebra2 A where
  liftFree2 :: f a b -> A f a b
liftFree2 = \f a b
fab -> (forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A ((forall (r :: * -> * -> *).
  Arrow r =>
  (forall x y. f x y -> r x y) -> r a b)
 -> A f a b)
-> (forall (r :: * -> * -> *).
    Arrow r =>
    (forall x y. f x y -> r x y) -> r a b)
-> A f a b
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> f a b -> r a b
forall x y. f x y -> r x y
k f a b
fab
  {-# INLINE liftFree2 #-}

  foldNatFree2 :: (forall x y. f x y -> d x y) -> A f a b -> d a b
foldNatFree2 forall x y. f x y -> d x y
fun (A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r a b
f) = (forall x y. f x y -> d x y) -> d a b
forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r a b
f forall x y. f x y -> d x y
fun
  {-# INLINE foldNatFree2 #-}

  codom2 :: Proof (AlgebraType A (A f)) (A f)
codom2  = Proof (AlgebraType A (A f)) (A f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: Proof (AlgebraType0 A f) (A f)
forget2 = Proof (AlgebraType0 A f) (A f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof