{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Control.Category.Free where

import qualified Control.Category as C
import Control.Category.Monoidal as C
import Control.Category.Cartesian as C
import Control.Category.Recursive as C
import Data.Kind ( Constraint )

-- Data kinds representing whether each constraint is required.
-- We could use 'Bool', but using separate Data Kinds helps a lot with producing nicer type errors.
data IsCategory = HasCategory | NoCategory
data IsSymmetricProduct = HasSymmetricProduct | NoSymmetricProduct
data IsSymmetricSum = HasSymmetricSum | NoSymmetricSum
data IsMonoidalProduct = HasMonoidalProduct | NoMonoidalProduct
data IsMonoidalSum = HasMonoidalSum | NoMonoidalSum
data IsCartesian = HasCartesian | NoCartesian
data IsCocartesian = HasCocartesian | NoCocartesian
data IsRecursive = HasRecursive | NoRecursive
data IsFixed = HasFixed | NoFixed

data Requirements =
    Req
        IsCategory
        IsSymmetricProduct
        IsSymmetricSum
        IsMonoidalProduct
        IsMonoidalSum
        IsCartesian
        IsCocartesian
        IsRecursive
        IsFixed

type family ConstraintsOf (x :: anykind) (k :: * -> * -> *) = (c :: Constraint) where
  -- The constraints of a 'Requirements' are the constriants of each class-requirement
  ConstraintsOf ('Req cat symP symS monP monS cart cocart rec fix) k = 
      ( ConstraintsOf cat k
      , ConstraintsOf symP k
      , ConstraintsOf symS k
      , ConstraintsOf monP k
      , ConstraintsOf monS k
      , ConstraintsOf cart k
      , ConstraintsOf cocart k
      , ConstraintsOf rec k
      , ConstraintsOf fix k
      )
  -- Each sub-requirement has an associated class
  ConstraintsOf 'HasCategory cat = C.Category cat
  ConstraintsOf 'HasSymmetricProduct cat = C.SymmetricProduct cat
  ConstraintsOf 'HasSymmetricSum cat = C.SymmetricSum cat
  ConstraintsOf 'HasMonoidalProduct cat = C.MonoidalProduct cat
  ConstraintsOf 'HasMonoidalSum cat = C.MonoidalSum cat
  ConstraintsOf 'HasCartesian cat = C.Cartesian cat
  ConstraintsOf 'HasCocartesian cat = C.Cocartesian cat
  ConstraintsOf 'HasRecursive cat = C.Recursive cat
  ConstraintsOf 'HasFixed cat = C.Fixed cat

  ConstraintsOf 'NoCategory cat = ()
  ConstraintsOf 'NoSymmetricProduct cat = ()
  ConstraintsOf 'NoSymmetricSum cat = ()
  ConstraintsOf 'NoMonoidalProduct cat = ()
  ConstraintsOf 'NoMonoidalSum cat = ()
  ConstraintsOf 'NoCartesian cat = ()
  ConstraintsOf 'NoCocartesian cat = ()
  ConstraintsOf 'NoRecursive cat = ()
  ConstraintsOf 'NoFixed cat = ()

type FreeFunction c a b =
    Catalyst
      ('Req
          'HasCategory
          'HasSymmetricProduct
          'HasSymmetricSum
          'HasMonoidalProduct
          'HasMonoidalSum
          'HasCartesian
          'HasCocartesian
          'HasRecursive
          'HasFixed
      ) c

data Catalyst (r :: Requirements) (p :: * -> * -> *) a b where
  ID :: (r ~ 'Req 'HasCategory symP symS monP monS cart cocart rec fix) => Catalyst r p x x
  Comp :: Catalyst ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p x y -> Catalyst ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p y z -> Catalyst ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p x z

  Swap :: (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS monP monS cart cocart rec fix) => Catalyst r p (a, b) (b, a)
  Reassoc :: (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS monP monS cart cocart rec fix) => Catalyst r p (a, (b, c)) ((a, b), c)

  SwapE :: (r ~ 'Req cat symP 'HasSymmetricSum monP monS cart cocart rec fix) => Catalyst r p (Either a b) (Either b a)
  ReassocE :: (r ~ 'Req cat symP 'HasSymmetricSum monP monS cart cocart rec fix) => Catalyst r p (Either a (Either b c)) (Either (Either a b) c)

  First :: (r ~ 'Req cat symP symS 'HasMonoidalProduct monS cart cocart rec fix) => Catalyst r p a b -> Catalyst r p (a, m) (b, m)
  Second :: (r ~ 'Req cat symP symS 'HasMonoidalProduct monS cart cocart rec fix) => Catalyst r p a b -> Catalyst r p (m, a) (m, b)
  -- (***)
  Alongside :: (r ~ 'Req cat symP symS 'HasMonoidalProduct monS cart cocart rec fix) => Catalyst r p a b -> Catalyst r p a' b' -> Catalyst r p (a, a') (b, b')
  -- (&&&)
  Fanout :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p a b -> Catalyst r p a b' -> Catalyst r p a (b, b')

  Left' :: (r ~ 'Req cat symP symS monP 'HasMonoidalSum cart cocart rec fix) => Catalyst r p a b -> Catalyst r p (Either a x) (Either b x)
  Right' :: (r ~ 'Req cat symP symS monP 'HasMonoidalSum cart cocart rec fix) => Catalyst r p a b -> Catalyst r p (Either x a) (Either x b)
  -- (+++)
  EitherOf :: (r ~ 'Req cat symP symS monP 'HasMonoidalSum cart cocart rec fix) => Catalyst r p a b -> Catalyst r p a' b' -> Catalyst r p (Either a a') (Either b b')
  -- (|||)
  Fanin :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p a b -> Catalyst r p a' b -> Catalyst r p (Either a a') b

  Copy :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p x (x, x)
  Consume :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p x ()
  Fst :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p (a, b) a
  Snd :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p (a, b) b

  InjectL :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p a (Either a b)
  InjectR :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p b (Either a b)
  Unify :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p (Either a a) a
  Tag :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p (Bool, a) (Either a a)

  RecurseL :: (r ~ 'Req cat symP symS monP monS cart cocart 'HasRecursive fix) => Catalyst r p (Either a d) (Either b d) -> Catalyst r p a b
  RecurseR :: (r ~ 'Req cat symP symS monP monS cart cocart 'HasRecursive fix) => Catalyst r p (Either d a) (Either d b) -> Catalyst r p a b

  FixL :: (r ~ 'Req cat symP symS monP monS cart cocart rec 'HasFixed) => Catalyst r p (a, d) (b, d) -> Catalyst r p a b
  FixR :: (r ~ 'Req cat symP symS monP monS cart cocart rec 'HasFixed) => Catalyst r p (d, a) (d, b) -> Catalyst r p a b

  LiftC :: p a b -> Catalyst r p a b

instance (forall x y. Show (c x y)) => Show (Catalyst r c a b) where
  show :: Catalyst r c a b -> String
show
    = \case
        Catalyst r c a b
Fst -> String
"fst"
        Catalyst r c a b
Snd -> String
"snd"
        Catalyst r c a b
Copy -> String
"copy"
        Catalyst r c a b
Consume -> String
"consume"
        Catalyst r c a b
Swap -> String
"swap"
        Catalyst r c a b
Reassoc -> String
"reassoc"
        Catalyst r c a b
SwapE -> String
"swapE"
        Catalyst r c a b
ReassocE -> String
"reassocE"

        Catalyst r c a b
InjectL -> String
"injectL"
        Catalyst r c a b
InjectR -> String
"injectR"
        Catalyst r c a b
Unify -> String
"unify"
        Catalyst r c a b
Tag -> String
"tag"
        (First Catalyst r c a b
l) -> String
"(first' " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b -> String
forall a. Show a => a -> String
show Catalyst r c a b
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (Second Catalyst r c a b
l) -> String
"(second' " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b -> String
forall a. Show a => a -> String
show Catalyst r c a b
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (Alongside Catalyst r c a b
l Catalyst r c a' b'
r) -> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b -> String
forall a. Show a => a -> String
show Catalyst r c a b
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" *** " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a' b' -> String
forall a. Show a => a -> String
show Catalyst r c a' b'
r String -> ShowS
forall a. Semigroup a => a -> a -> a
<>  String
")"
        (Fanout Catalyst r c a b
l Catalyst r c a b'
r) -> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b -> String
forall a. Show a => a -> String
show Catalyst r c a b
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" &&& " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b' -> String
forall a. Show a => a -> String
show Catalyst r c a b'
r  String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (Left' Catalyst r c a b
l) -> String
"(left " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b -> String
forall a. Show a => a -> String
show Catalyst r c a b
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (Right' Catalyst r c a b
r) -> String
"(right " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b -> String
forall a. Show a => a -> String
show Catalyst r c a b
r String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (EitherOf Catalyst r c a b
l Catalyst r c a' b'
r) -> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b -> String
forall a. Show a => a -> String
show Catalyst r c a b
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" +++ " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a' b' -> String
forall a. Show a => a -> String
show Catalyst r c a' b'
r String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (Fanin Catalyst r c a b
l Catalyst r c a' b
r) -> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a b -> String
forall a. Show a => a -> String
show Catalyst r c a b
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" +++ " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c a' b -> String
forall a. Show a => a -> String
show Catalyst r c a' b
r String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (LiftC c a b
cab) -> c a b -> String
forall a. Show a => a -> String
show c a b
cab
        Catalyst r c a b
ID -> String
"id"
        (Comp Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a y
l Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c y b
r) -> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a y
-> String
forall a. Show a => a -> String
show Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a y
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" >>> " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c y b
-> String
forall a. Show a => a -> String
show Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c y b
r String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (RecurseL Catalyst r c (Either a d) (Either b d)
l) -> String
"(recurseR " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c (Either a d) (Either b d) -> String
forall a. Show a => a -> String
show Catalyst r c (Either a d) (Either b d)
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (RecurseR Catalyst r c (Either d a) (Either d b)
r) -> String
"(recurseL " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c (Either d a) (Either d b) -> String
forall a. Show a => a -> String
show Catalyst r c (Either d a) (Either d b)
r String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (FixL Catalyst r c (a, d) (b, d)
l) -> String
"(fixL " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c (a, d) (b, d) -> String
forall a. Show a => a -> String
show Catalyst r c (a, d) (b, d)
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        (FixR Catalyst r c (d, a) (d, b)
r) -> String
"(fixR " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Catalyst r c (d, a) (d, b) -> String
forall a. Show a => a -> String
show Catalyst r c (d, a) (d, b)
r String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"

runFree :: forall r p c a b. (ConstraintsOf r p) => (forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree :: (forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp = \case
  LiftC c a b
c -> c a b -> p a b
forall x y. c x y -> p x y
interp c a b
c
  Catalyst r c a b
Fst -> p a b
forall (k :: * -> * -> *) l r. Cartesian k => k (l, r) l
fst'
  Catalyst r c a b
Snd -> p a b
forall (k :: * -> * -> *) l r. Cartesian k => k (l, r) r
snd'
  Catalyst r c a b
Copy -> p a b
forall (k :: * -> * -> *) a. Cartesian k => k a (a, a)
copy
  Catalyst r c a b
Consume -> p a b
forall (k :: * -> * -> *) a. Cartesian k => k a ()
consume
  Catalyst r c a b
Swap -> p a b
forall (k :: * -> * -> *) l r.
SymmetricProduct k =>
k (l, r) (r, l)
swap
  Catalyst r c a b
SwapE -> p a b
forall (k :: * -> * -> *) l r.
SymmetricSum k =>
k (Either l r) (Either r l)
swapE
  Catalyst r c a b
Reassoc -> p a b
forall (k :: * -> * -> *) a b c.
SymmetricProduct k =>
k (a, (b, c)) ((a, b), c)
reassoc
  Catalyst r c a b
ReassocE -> p a b
forall (k :: * -> * -> *) a b c.
SymmetricSum k =>
k (Either a (Either b c)) (Either (Either a b) c)
reassocE
  Catalyst r c a b
InjectL -> p a b
forall (k :: * -> * -> *) a b. Cocartesian k => k a (Either a b)
injectL
  Catalyst r c a b
InjectR -> p a b
forall (k :: * -> * -> *) a b. Cocartesian k => k a (Either b a)
injectR
  Catalyst r c a b
Unify -> p a b
forall (k :: * -> * -> *) a. Cocartesian k => k (Either a a) a
unify
  Catalyst r c a b
Tag -> p a b
forall (k :: * -> * -> *) a.
Cocartesian k =>
k (Bool, a) (Either a a)
tag
  First Catalyst r c a b
p -> p a b -> p (a, m) (b, m)
forall (k :: * -> * -> *) a b c.
MonoidalProduct k =>
k a b -> k (a, c) (b, c)
first' ((forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b
p)
  Second Catalyst r c a b
p -> p a b -> p (m, a) (m, b)
forall (k :: * -> * -> *) a b c.
MonoidalProduct k =>
k a b -> k (c, a) (c, b)
second' ((forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b
p)
  Alongside Catalyst r c a b
l Catalyst r c a' b'
r -> (forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b
l p a b -> p a' b' -> p (a, a') (b, b')
forall (k :: * -> * -> *) al bl ar br.
MonoidalProduct k =>
k al bl -> k ar br -> k (al, ar) (bl, br)
C.*** (forall x y. c x y -> p x y) -> Catalyst r c a' b' -> p a' b'
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a' b'
r
  Fanout Catalyst r c a b
l Catalyst r c a b'
r -> (forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b
l p a b -> p a b' -> p a (b, b')
forall (k :: * -> * -> *) a l r.
Cartesian k =>
k a l -> k a r -> k a (l, r)
C.&&& (forall x y. c x y -> p x y) -> Catalyst r c a b' -> p a b'
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b'
r
  Left' Catalyst r c a b
p -> p a b -> p (Either a x) (Either b x)
forall (k :: * -> * -> *) a b c.
MonoidalSum k =>
k a b -> k (Either a c) (Either b c)
left ((forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b
p)
  Right' Catalyst r c a b
p -> p a b -> p (Either x a) (Either x b)
forall (k :: * -> * -> *) a b c.
MonoidalSum k =>
k a b -> k (Either c a) (Either c b)
right ((forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b
p)
  Fanin Catalyst r c a b
l Catalyst r c a' b
r -> (forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b
l p a b -> p a' b -> p (Either a a') b
forall (k :: * -> * -> *) al b ar.
Cocartesian k =>
k al b -> k ar b -> k (Either al ar) b
C.||| (forall x y. c x y -> p x y) -> Catalyst r c a' b -> p a' b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a' b
r
  EitherOf Catalyst r c a b
l Catalyst r c a' b'
r -> (forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a b
l p a b -> p a' b' -> p (Either a a') (Either b b')
forall (k :: * -> * -> *) al bl ar br.
MonoidalSum k =>
k al bl -> k ar br -> k (Either al ar) (Either bl br)
C.+++ (forall x y. c x y -> p x y) -> Catalyst r c a' b' -> p a' b'
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c a' b'
r
  Comp Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a y
l Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c y b
r -> (forall x y. c x y -> p x y)
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a y
-> p a y
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a y
l p a y -> p y b -> p a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
C.>>> (forall x y. c x y -> p x y)
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c y b
-> p y b
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c y b
r
  Catalyst r c a b
ID -> p a b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
C.id
  RecurseL Catalyst r c (Either a d) (Either b d)
l -> p (Either a d) (Either b d) -> p a b
forall (k :: * -> * -> *) a s b.
Recursive k =>
k (Either a s) (Either b s) -> k a b
recurseL ((forall x y. c x y -> p x y)
-> Catalyst r c (Either a d) (Either b d)
-> p (Either a d) (Either b d)
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c (Either a d) (Either b d)
l)
  RecurseR Catalyst r c (Either d a) (Either d b)
r -> p (Either d a) (Either d b) -> p a b
forall (k :: * -> * -> *) s a b.
Recursive k =>
k (Either s a) (Either s b) -> k a b
recurseR ((forall x y. c x y -> p x y)
-> Catalyst r c (Either d a) (Either d b)
-> p (Either d a) (Either d b)
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c (Either d a) (Either d b)
r)
  FixL Catalyst r c (a, d) (b, d)
l -> p (a, d) (b, d) -> p a b
forall (k :: * -> * -> *) a s b.
Fixed k =>
k (a, s) (b, s) -> k a b
fixL ((forall x y. c x y -> p x y)
-> Catalyst r c (a, d) (b, d) -> p (a, d) (b, d)
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c (a, d) (b, d)
l)
  FixR Catalyst r c (d, a) (d, b)
r -> p (d, a) (d, b) -> p a b
forall (k :: * -> * -> *) s a b.
Fixed k =>
k (s, a) (s, b) -> k a b
fixR ((forall x y. c x y -> p x y)
-> Catalyst r c (d, a) (d, b) -> p (d, a) (d, b)
forall (r :: Requirements) (p :: * -> * -> *) (c :: * -> * -> *) a
       b.
ConstraintsOf r p =>
(forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
runFree forall x y. c x y -> p x y
interp Catalyst r c (d, a) (d, b)
r)

liftC :: c a b -> Catalyst r c a b
liftC :: c a b -> Catalyst r c a b
liftC = c a b -> Catalyst r c a b
forall (p :: * -> * -> *) a b (r :: Requirements).
p a b -> Catalyst r p a b
LiftC

instance (r ~ 'Req 'HasCategory symP symS monP monS cart cocart rec fix)
         => C.Category (Catalyst r c) where
  id :: Catalyst r c a a
id = Catalyst r c a a
forall (r :: Requirements) (symP :: IsSymmetricProduct)
       (symS :: IsSymmetricSum) (monP :: IsMonoidalProduct)
       (monS :: IsMonoidalSum) (cart :: IsCartesian)
       (symP :: IsCocartesian) (symS :: IsRecursive) (monP :: IsFixed)
       (p :: * -> * -> *) x.
(r ~ 'Req 'HasCategory symP symS monP monS cart symP symS monP) =>
Catalyst r p x x
ID
  . :: Catalyst r c b c -> Catalyst r c a b -> Catalyst r c a c
(.) = (Catalyst
   ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a b
 -> Catalyst
      ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c b c
 -> Catalyst
      ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a c)
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c b c
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a b
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a b
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c b c
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) c a c
forall (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cocart :: IsCocartesian)
       (rec :: IsRecursive) (fix :: IsFixed) (p :: * -> * -> *) x y z.
Catalyst
  ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p x y
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p y z
-> Catalyst
     ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p x z
Comp

instance (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS 'HasMonoidalProduct monS 'HasCartesian cocart rec fix)
  => C.Cartesian (Catalyst r c) where
  copy :: Catalyst r c a (a, a)
copy = Catalyst r c a (a, a)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cocart :: IsCocartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) x.
(r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) =>
Catalyst r p x (x, x)
Copy
  consume :: Catalyst r c a ()
consume = Catalyst r c a ()
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cocart :: IsCocartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) x.
(r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) =>
Catalyst r p x ()
Consume
  fst' :: Catalyst r c (l, r) l
fst' = Catalyst r c (l, r) l
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cocart :: IsCocartesian) (cat :: IsRecursive) (symP :: IsFixed)
       (p :: * -> * -> *) a monP.
(r ~ 'Req cat symP symS monP monS 'HasCartesian cocart cat symP) =>
Catalyst r p (a, monP) a
Fst
  snd' :: Catalyst r c (l, r) r
snd' = Catalyst r c (l, r) r
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cocart :: IsCocartesian) (cat :: IsRecursive) (symP :: IsFixed)
       (p :: * -> * -> *) a b.
(r ~ 'Req cat symP symS monP monS 'HasCartesian cocart cat symP) =>
Catalyst r p (a, b) b
Snd

instance (r ~ 'Req 'HasCategory symP 'HasSymmetricSum monP 'HasMonoidalSum cart 'HasCocartesian rec fix)
         => C.Cocartesian (Catalyst r c) where
  injectL :: Catalyst r c a (Either a b)
injectL = Catalyst r c a (Either a b)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cat :: IsRecursive) (symP :: IsFixed)
       (p :: * -> * -> *) a monP.
(r ~ 'Req cat symP symS monP monS cart 'HasCocartesian cat symP) =>
Catalyst r p a (Either a monP)
InjectL
  injectR :: Catalyst r c a (Either b a)
injectR = Catalyst r c a (Either b a)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cat :: IsRecursive) (symP :: IsFixed)
       (p :: * -> * -> *) b monP.
(r ~ 'Req cat symP symS monP monS cart 'HasCocartesian cat symP) =>
Catalyst r p b (Either monP b)
InjectR
  unify :: Catalyst r c (Either a a) a
unify = Catalyst r c (Either a a) a
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) a.
(r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) =>
Catalyst r p (Either a a) a
Unify
  tag :: Catalyst r c (Bool, a) (Either a a)
tag = Catalyst r c (Bool, a) (Either a a)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) monP.
(r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) =>
Catalyst r p (Bool, monP) (Either monP monP)
Tag

instance (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS monP monS cart cocart rec fix) => C.SymmetricProduct (Catalyst r c) where
  swap :: Catalyst r c (l, r) (r, l)
swap = Catalyst r c (l, r) (r, l)
forall (r :: Requirements) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cocart :: IsCocartesian)
       (rec :: IsRecursive) (fix :: IsFixed) (p :: * -> * -> *) monS cart.
(r
 ~ 'Req
     'HasCategory
     'HasSymmetricProduct
     symS
     monP
     monS
     cart
     cocart
     rec
     fix) =>
Catalyst r p (monS, cart) (cart, monS)
Swap
  reassoc :: Catalyst r c (a, (b, c)) ((a, b), c)
reassoc = Catalyst r c (a, (b, c)) ((a, b), c)
forall (r :: Requirements) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cocart :: IsCocartesian)
       (rec :: IsRecursive) (cat :: IsFixed) (p :: * -> * -> *) a b c.
(r
 ~ 'Req
     'HasCategory
     'HasSymmetricProduct
     symS
     monP
     monS
     cart
     cocart
     rec
     cat) =>
Catalyst r p (a, (b, c)) ((a, b), c)
Reassoc

instance (r ~ 'Req 'HasCategory symP 'HasSymmetricSum monP monS cart cocart rec fix) => C.SymmetricSum (Catalyst r c) where
  swapE :: Catalyst r c (Either l r) (Either r l)
swapE = Catalyst r c (Either l r) (Either r l)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (monP :: IsMonoidalProduct)
       (monS :: IsMonoidalSum) (cart :: IsCartesian)
       (cocart :: IsCocartesian) (cat :: IsRecursive) (symP :: IsFixed)
       (p :: * -> * -> *) a b.
(r
 ~ 'Req cat symP 'HasSymmetricSum monP monS cart cocart cat symP) =>
Catalyst r p (Either a b) (Either b a)
SwapE
  reassocE :: Catalyst r c (Either a (Either b c)) (Either (Either a b) c)
reassocE = Catalyst r c (Either a (Either b c)) (Either (Either a b) c)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (monP :: IsMonoidalProduct)
       (monS :: IsMonoidalSum) (cart :: IsCartesian)
       (cocart :: IsCocartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) symS monS cart.
(r
 ~ 'Req cat symP 'HasSymmetricSum monP monS cart cocart rec fix) =>
Catalyst
  r
  p
  (Either symS (Either monS cart))
  (Either (Either symS monS) cart)
ReassocE

instance (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS 'HasMonoidalProduct monS cart cocart rec fix) => C.MonoidalProduct (Catalyst r c) where
  *** :: Catalyst r c al bl
-> Catalyst r c ar br -> Catalyst r c (al, ar) (bl, br)
(***) = Catalyst r c al bl
-> Catalyst r c ar br -> Catalyst r c (al, ar) (bl, br)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (a :: IsSymmetricSum)
       (b :: IsMonoidalSum) (m :: IsCartesian) (cocart :: IsCocartesian)
       (rec :: IsRecursive) (fix :: IsFixed) (p :: * -> * -> *) a b a' b'.
(r ~ 'Req cat symP a 'HasMonoidalProduct b m cocart rec fix) =>
Catalyst r p a b
-> Catalyst r p a' b' -> Catalyst r p (a, a') (b, b')
Alongside
  first' :: Catalyst r c a b -> Catalyst r c (a, c) (b, c)
first' = Catalyst r c a b -> Catalyst r c (a, c) (b, c)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monS :: IsMonoidalSum) (cart :: IsCartesian)
       (cocart :: IsCocartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) symS monS cart.
(r
 ~ 'Req
     cat symP symS 'HasMonoidalProduct monS cart cocart rec fix) =>
Catalyst r p symS monS -> Catalyst r p (symS, cart) (monS, cart)
First
  second' :: Catalyst r c a b -> Catalyst r c (c, a) (c, b)
second' = Catalyst r c a b -> Catalyst r c (c, a) (c, b)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monS :: IsMonoidalSum) (cart :: IsCartesian)
       (cocart :: IsCocartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) a b m.
(r
 ~ 'Req
     cat symP symS 'HasMonoidalProduct monS cart cocart rec fix) =>
Catalyst r p a b -> Catalyst r p (m, a) (m, b)
Second

instance (r ~ 'Req 'HasCategory symP 'HasSymmetricSum monP 'HasMonoidalSum cart cocart rec fix) => C.MonoidalSum (Catalyst r c) where
  +++ :: Catalyst r c al bl
-> Catalyst r c ar br -> Catalyst r c (Either al ar) (Either bl br)
(+++) = Catalyst r c al bl
-> Catalyst r c ar br -> Catalyst r c (Either al ar) (Either bl br)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (a :: IsSymmetricSum)
       (b :: IsMonoidalProduct) (x :: IsCartesian)
       (cocart :: IsCocartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) a b a' b'.
(r ~ 'Req cat symP a b 'HasMonoidalSum x cocart rec fix) =>
Catalyst r p a b
-> Catalyst r p a' b' -> Catalyst r p (Either a a') (Either b b')
EitherOf
  left :: Catalyst r c a b -> Catalyst r c (Either a c) (Either b c)
left = Catalyst r c a b -> Catalyst r c (Either a c) (Either b c)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (cart :: IsCartesian)
       (cocart :: IsCocartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) symS monP cart.
(r
 ~ 'Req cat symP symS monP 'HasMonoidalSum cart cocart rec fix) =>
Catalyst r p symS monP
-> Catalyst r p (Either symS cart) (Either monP cart)
Left'
  right :: Catalyst r c a b -> Catalyst r c (Either c a) (Either c b)
right = Catalyst r c a b -> Catalyst r c (Either c a) (Either c b)
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (cart :: IsCartesian)
       (cocart :: IsCocartesian) (rec :: IsRecursive) (fix :: IsFixed)
       (p :: * -> * -> *) a b x.
(r
 ~ 'Req cat symP symS monP 'HasMonoidalSum cart cocart rec fix) =>
Catalyst r p a b -> Catalyst r p (Either x a) (Either x b)
Right'

instance (r ~ 'Req 'HasCategory symP symS monP monS cart cocart 'HasRecursive fix) => Recursive (Catalyst r c) where
  recurseL :: Catalyst r c (Either a s) (Either b s) -> Catalyst r c a b
recurseL = Catalyst r c (Either a s) (Either b s) -> Catalyst r c a b
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cocart :: IsCocartesian) (fix :: IsFixed)
       (p :: * -> * -> *) a d b.
(r ~ 'Req cat symP symS monP monS cart cocart 'HasRecursive fix) =>
Catalyst r p (Either a d) (Either b d) -> Catalyst r p a b
RecurseL
  recurseR :: Catalyst r c (Either s a) (Either s b) -> Catalyst r c a b
recurseR = Catalyst r c (Either s a) (Either s b) -> Catalyst r c a b
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cocart :: IsCocartesian) (fix :: IsFixed)
       (p :: * -> * -> *) symS a b.
(r ~ 'Req cat symP symS monP monS cart cocart 'HasRecursive fix) =>
Catalyst r p (Either symS a) (Either symS b) -> Catalyst r p a b
RecurseR

instance (r ~ 'Req 'HasCategory symP symS monP monS cart cocart rec 'HasFixed) => Fixed (Catalyst r c) where
  fixL :: Catalyst r c (a, s) (b, s) -> Catalyst r c a b
fixL = Catalyst r c (a, s) (b, s) -> Catalyst r c a b
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cocart :: IsCocartesian)
       (rec :: IsRecursive) (p :: * -> * -> *) a d b.
(r ~ 'Req cat symP symS monP monS cart cocart rec 'HasFixed) =>
Catalyst r p (a, d) (b, d) -> Catalyst r p a b
FixL
  fixR :: Catalyst r c (s, a) (s, b) -> Catalyst r c a b
fixR = Catalyst r c (s, a) (s, b) -> Catalyst r c a b
forall (r :: Requirements) (cat :: IsCategory)
       (symP :: IsSymmetricProduct) (symS :: IsSymmetricSum)
       (monP :: IsMonoidalProduct) (monS :: IsMonoidalSum)
       (cart :: IsCartesian) (cocart :: IsCocartesian)
       (rec :: IsRecursive) (p :: * -> * -> *) d a b.
(r ~ 'Req cat symP symS monP monS cart cocart rec 'HasFixed) =>
Catalyst r p (d, a) (d, b) -> Catalyst r p a b
FixR