{-# 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 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
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
)
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