{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Helper.CCC
  ( toCCC
  , lam
  , ($)
  , lift
  , pattern (:&)
  , Free (Lft, Rgt)
  , either
  , InitF
  , TermF
  , type (*!)
  , type (+)
  , type (-->)
  , FK (..)
  ) where

import Data.Kind (Constraint, Type)
import Prelude (type (~))
import Prelude qualified as P

import Proarrow.Category.Monoidal.Distributive (distLProd)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), UN)
import Proarrow.Object (Obj, obj)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), lft', rgt')
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..), fst', snd')
import Proarrow.Object.Exponential (BiCCC, Closed (..), eval)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..), terminate')

type Cast :: forall {k}. [FK k] -> [FK k] -> Constraint
class Cast i j where
  cast :: (IsFK a) => Free j a -> Free i a

instance {-# OVERLAPPABLE #-} (Cast i j, (a ': i) ~ i', IsFK a, IsFKs i) => Cast i' j where
  cast :: forall (a :: FK k). IsFK a => Free j a -> Free i' a
cast = Free i a -> Free (a : i) a
forall {k} (a :: FK k) (b :: FK k) (b :: [FK k]).
(IsFK a, IsFK b, IsFKs b) =>
Free b b -> Free (a : b) b
Tail (Free i a -> Free (a : i) a)
-> (Free j a -> Free i a) -> Free j a -> Free (a : i) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (i :: [FK k]) (j :: [FK k]) (a :: FK k).
(Cast i j, IsFK a) =>
Free j a -> Free i a
forall {k} (i :: [FK k]) (j :: [FK k]) (a :: FK k).
(Cast i j, IsFK a) =>
Free j a -> Free i a
cast @i @j

instance Cast i i where
  cast :: forall (a :: FK k). IsFK a => Free i a -> Free i a
cast Free i a
f = Free i a
f

pattern Uncurry :: (IsFK (a :: FK k), IsFK (b :: FK k), IsFKs (i :: [FK k]), Closed k) => Free i (a --> b) -> Free (a : i) b
pattern $mUncurry :: forall {r} {k} {a :: FK k} {b :: FK k} {i :: [FK k]}.
(IsFK a, IsFK b, IsFKs i, Closed k) =>
Free (a : i) b -> (Free i (a --> b) -> r) -> ((# #) -> r) -> r
$bUncurry :: forall k (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i, Closed k) =>
Free i (a --> b) -> Free (a : i) b
Uncurry f = Apply (Tail f) (Head Id)

lam
  :: forall {k} a b i
   . (IsFK a, IsFK b, IsFKs i)
  => ((forall (x :: [FK k]). (Cast x (a ': i)) => Free x a) -> Free (a ': i) b)
  -> Free i (a --> b)
lam :: forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i) =>
((forall (x :: [FK k]). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a --> b)
lam (forall (x :: [FK k]). Cast x (a : i) => Free x a)
-> Free (a : i) b
f = Free (a : i) b -> Free i (a --> b)
forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i) =>
Free (a : i) b -> Free i (a --> b)
Curry ((forall (x :: [FK k]). Cast x (a : i) => Free x a)
-> Free (a : i) b
f Free x a
forall (x :: [FK k]). Cast x (a : i) => Free x a
xa)
  where
    xa :: forall (x :: [FK k]). (Cast x (a ': i)) => Free x a
    xa :: forall (x :: [FK k]). Cast x (a : i) => Free x a
xa = forall (i :: [FK k]) (j :: [FK k]) (a :: FK k).
(Cast i j, IsFK a) =>
Free j a -> Free i a
forall {k} (i :: [FK k]) (j :: [FK k]) (a :: FK k).
(Cast i j, IsFK a) =>
Free j a -> Free i a
cast @x @(a ': i) (Free '[a] a -> Free (a : i) a
forall {k} (a :: FK k) (b :: FK k) (b :: [FK k]).
(IsFK a, IsFK b, IsFKs b) =>
Free '[a] b -> Free (a : b) b
Head Free '[a] a
forall {k} (a :: FK k). IsFK a => Free '[a] a
Id)

infixr 0 $
($) :: (IsFK a, IsFK b, IsFKs i) => Free i (a --> b) -> Free i a -> Free i b
$ :: forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i) =>
Free i (a --> b) -> Free i a -> Free i b
($) = Free i (a --> b) -> Free i a -> Free i b
forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i) =>
Free i (a --> b) -> Free i a -> Free i b
Apply

lift :: a ~> b -> Free i (F a) -> Free i (F b)
lift :: forall {k} (a :: k) (b :: k) (i :: [FK k]).
(a ~> b) -> Free i ('F a) -> Free i ('F b)
lift = (a ~> b) -> Free i ('F a) -> Free i ('F b)
forall {k} (a :: k) (b :: k) (i :: [FK k]).
(a ~> b) -> Free i ('F a) -> Free i ('F b)
L

fstSnd :: (IsFK a, IsFK b, IsFKs i) => Free i (a *! b) -> (Free i a, Free i b)
fstSnd :: forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i) =>
Free i (a *! b) -> (Free i a, Free i b)
fstSnd Free i (a *! b)
f = (Free i (a *! b) -> Free i a
forall {k} (a :: FK k) (a :: FK k) (i :: [FK k]).
(IsFK a, IsFK a, IsFKs i) =>
Free i (a *! a) -> Free i a
Fst Free i (a *! b)
f, Free i (a *! b) -> Free i b
forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i) =>
Free i (a *! b) -> Free i b
Snd Free i (a *! b)
f)

pattern (:&) :: (IsFK a, IsFK b, IsFKs i) => Free i a -> Free i b -> Free i (a *! b)
pattern x $m:& :: forall {r} {k} {a :: FK k} {b :: FK k} {i :: [FK k]}.
(IsFK a, IsFK b, IsFKs i) =>
Free i (a *! b) -> (Free i a -> Free i b -> r) -> ((# #) -> r) -> r
$b:& :: forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i) =>
Free i a -> Free i b -> Free i (a *! b)
:& y <- (fstSnd -> (x, y))
  where
    Free i a
x :& Free i b
y = Free i a -> Free i b -> Free i (a *! b)
forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i) =>
Free i a -> Free i b -> Free i (a *! b)
Prd Free i a
x Free i b
y

{-# COMPLETE (:&) #-}

either
  :: forall {k} (a :: FK k) b c i
   . (IsFK a, IsFK b, IsFK c, IsFKs i, Closed k)
  => Free i (a --> c)
  -> Free i (b --> c)
  -> Free i (a + b)
  -> Free i c
either :: forall {k} (a :: FK k) (b :: FK k) (c :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFK c, IsFKs i, Closed k) =>
Free i (a --> c) -> Free i (b --> c) -> Free i (a + b) -> Free i c
either Free i (a --> c)
f Free i (b --> c)
g Free i (a + b)
m = Free i (a + b) -> Free (a : i) c -> Free (b : i) c -> Free i c
forall {k} (a :: FK k) (b :: FK k) (c :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFK c, IsFKs i) =>
Free i (a + b) -> Free (a : i) c -> Free (b : i) c -> Free i c
Sum Free i (a + b)
m (Free i (a --> c) -> Free (a : i) c
forall k (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i, Closed k) =>
Free i (a --> b) -> Free (a : i) b
Uncurry Free i (a --> c)
f) (Free i (b --> c) -> Free (b : i) c
forall k (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i, Closed k) =>
Free i (a --> b) -> Free (a : i) b
Uncurry Free i (b --> c)
g)

type MultiCat k = [k] -> k -> Type
data FK k = F k
type instance UN F (F a) = a

infixr 2 -->

data family InitF :: k
data family TermF :: k
data family (+) (a :: k) (b :: k) :: k
data family (*!) (a :: k) (b :: k) :: k
data family (-->) (a :: k) (b :: k) :: k

type family Mul as where
  Mul '[] = TermF
  Mul '[a] = a
  Mul (a ': as) = Mul as *! a

data Free :: MultiCat (FK k) where
  Id :: (IsFK a) => Free '[a] a
  L :: a ~> b -> Free i (F a) -> Free i (F b)
  Head :: (IsFK a, IsFK b, IsFKs i) => Free '[a] b -> Free (a ': i) b
  Tail :: (IsFK a, IsFK b, IsFKs i) => Free i b -> Free (a ': i) b
  Ini :: (IsFK a, IsFKs i) => Free i InitF -> Free i a
  Ter :: (IsFKs i) => Free i TermF
  Fst :: (IsFK a, IsFK b, IsFKs i) => Free i (a *! b) -> Free i a
  Snd :: (IsFK a, IsFK b, IsFKs i) => Free i (a *! b) -> Free i b
  Prd :: (IsFK a, IsFK b, IsFKs i) => Free i a -> Free i b -> Free i (a *! b)
  Lft :: (IsFK a, IsFK b, IsFKs i) => Free i a -> Free i (a + b)
  Rgt :: (IsFK a, IsFK b, IsFKs i) => Free i b -> Free i (a + b)
  Sum :: (IsFK a, IsFK b, IsFK c, IsFKs i) => Free i (a + b) -> Free (a ': i) c -> Free (b ': i) c -> Free i c
  Curry :: (IsFK a, IsFK b, IsFKs i) => Free (a ': i) b -> Free i (a --> b)
  Apply :: (IsFK a, IsFK b, IsFKs i) => Free i (a --> b) -> Free i a -> Free i b

instance P.Show (Free a b) where
  show :: Free a b -> String
show Free a b
Id = String
"fst"
  show (L a ~> b
_ Free a ('F a)
Id) = String
"<arrow>"
  show (L a ~> b
_ Free a ('F a)
f) = String
"(<arrow> . " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a ('F a) -> String
forall a. Show a => a -> String
P.show Free a ('F a)
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Head Free '[a] b
f) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free '[a] b -> String
forall a. Show a => a -> String
P.show Free '[a] b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" . snd)"
  show (Tail Free i b
f) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free i b -> String
forall a. Show a => a -> String
P.show Free i b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" . fst)"
  show (Ini Free a InitF
f) = String
"(initiate . " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a InitF -> String
forall a. Show a => a -> String
P.show Free a InitF
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show Free a b
Ter = String
"terminate"
  show (Lft Free a a
Id) = String
"lft"
  show (Lft Free a a
f) = String
"(lft . " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a a -> String
forall a. Show a => a -> String
P.show Free a a
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Rgt Free a b
Id) = String
"rgt"
  show (Rgt Free a b
f) = String
"(rgt . " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a b -> String
forall a. Show a => a -> String
P.show Free a b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Sum Free a (a + b)
Id Free (a : a) b
f Free (b : a) b
g) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free (a : a) b -> String
forall a. Show a => a -> String
P.show Free (a : a) b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" ||| " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free (b : a) b -> String
forall a. Show a => a -> String
P.show Free (b : a) b
g String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Sum Free a (a + b)
m Free (a : a) b
f Free (b : a) b
g) = String
"((" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free (a : a) b -> String
forall a. Show a => a -> String
P.show Free (a : a) b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" ||| " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free (b : a) b -> String
forall a. Show a => a -> String
P.show Free (b : a) b
g String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
") . " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a (a + b) -> String
forall a. Show a => a -> String
P.show Free a (a + b)
m String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Fst Free a (b *! b)
Id) = String
"fst"
  show (Fst Free a (b *! b)
f) = String
"(fst . " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a (b *! b) -> String
forall a. Show a => a -> String
P.show Free a (b *! b)
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Snd Free a (a *! b)
Id) = String
"snd"
  show (Snd Free a (a *! b)
f) = String
"(snd . " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a (a *! b) -> String
forall a. Show a => a -> String
P.show Free a (a *! b)
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Prd Free a a
f Free a b
g) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a a -> String
forall a. Show a => a -> String
P.show Free a a
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" &&& " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a b -> String
forall a. Show a => a -> String
P.show Free a b
g String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Curry Free (a : a) b
f) = String
"(curry " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free (a : a) b -> String
forall a. Show a => a -> String
P.show Free (a : a) b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Apply Free a (a --> b)
f Free a a
a) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a (a --> b) -> String
forall a. Show a => a -> String
P.show Free a (a --> b)
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" $ " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Free a a -> String
forall a. Show a => a -> String
P.show Free a a
a String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"

type family FromFree (t :: FK k) :: k
type instance FromFree (F a) = a
type instance FromFree InitF = InitialObject
type instance FromFree TermF = TerminalObject
type instance FromFree (a + b) = FromFree a || FromFree b
type instance FromFree (a *! b) = FromFree a && FromFree b
type instance FromFree (a --> b) = FromFree a ~~> FromFree b

type IsFKs :: forall {k}. [FK k] -> Constraint
class (Cartesian k) => IsFKs (i :: [FK k]) where
  head :: (IsFK b) => FromFree (Mul (b : i)) ~> FromFree b
  tail :: (IsFK b) => FromFree (Mul (b : i)) ~> FromFree (Mul i)
  snoc :: (IsFK b) => FromFree (Mul i) && FromFree b ~> FromFree (Mul (b : i))
  fromFreeObjs :: Obj (FromFree (Mul i))
  fromFreeObjs1 :: (IsFK b) => Obj (FromFree (Mul (b : i)))
instance (Cartesian k) => IsFKs ('[] :: [FK k]) where
  head :: forall (b :: FK k). IsFK b => FromFree (Mul '[b]) ~> FromFree b
head @b = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
  tail :: forall (b :: FK k).
IsFK b =>
FromFree (Mul '[b]) ~> FromFree (Mul '[])
tail @b = FromFree b ~> TerminalObject
(Ob (FromFree b), Ob (FromFree b)) => FromFree b ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate ((Ob (FromFree b), Ob (FromFree b)) =>
 FromFree b ~> TerminalObject)
-> (FromFree b ~> FromFree b) -> FromFree b ~> TerminalObject
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
  snoc :: forall (b :: FK k).
IsFK b =>
(FromFree (Mul '[]) && FromFree b) ~> FromFree (Mul '[b])
snoc @b = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @TerminalObject ((Ob (FromFree b), Ob (FromFree b)) =>
 (TerminalObject && FromFree b) ~> FromFree b)
-> (FromFree b ~> FromFree b)
-> (TerminalObject && FromFree b) ~> FromFree b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
  fromFreeObjs :: Obj (FromFree (Mul '[]))
fromFreeObjs = TerminalObject ~> TerminalObject
Obj (FromFree (Mul '[]))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  fromFreeObjs1 :: forall (b :: FK k). IsFK b => Obj (FromFree (Mul '[b]))
fromFreeObjs1 @b = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
instance (IsFKs i, IsFK (a :: FK k)) => IsFKs (a : i) where
  head :: forall (b :: FK k).
IsFK b =>
FromFree (Mul (b : a : i)) ~> FromFree b
head @b = Obj (FromFree (Mul (a : i)))
-> (FromFree b ~> FromFree b)
-> (FromFree (Mul (a : i)) && FromFree b) ~> FromFree b
forall {k} (a :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
Obj a -> (b ~> b') -> (a && b) ~> b'
snd' (forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
fromFreeObjs1 @i @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b)
  tail :: forall (b :: FK k).
IsFK b =>
FromFree (Mul (b : a : i)) ~> FromFree (Mul (a : i))
tail @b = Obj (FromFree (Mul (a : i)))
-> Obj (FromFree b)
-> (FromFree (Mul (a : i)) && FromFree b) ~> FromFree (Mul (a : i))
forall {k} (a :: k) (a' :: k) (b :: k).
HasBinaryProducts k =>
(a ~> a') -> Obj b -> (a && b) ~> a'
fst' (forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
fromFreeObjs1 @i @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b)
  snoc :: forall (b :: FK k).
IsFK b =>
(FromFree (Mul (a : i)) && FromFree b)
~> FromFree (Mul (b : a : i))
snoc @b = forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
fromFreeObjs1 @i @a Obj (FromFree (Mul (a : i)))
-> (FromFree b ~> FromFree b)
-> (FromFree (Mul (a : i)) && FromFree b)
   ~> (FromFree (Mul (a : i)) && FromFree b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
  fromFreeObjs :: Obj (FromFree (Mul (a : i)))
fromFreeObjs = forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
fromFreeObjs1 @i @a
  fromFreeObjs1 :: forall (b :: FK k). IsFK b => Obj (FromFree (Mul (b : a : i)))
fromFreeObjs1 @b = forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
Obj (FromFree (Mul (b : i)))
fromFreeObjs1 @i @a Obj (FromFree (Mul (a : i)))
-> (FromFree b ~> FromFree b)
-> (FromFree (Mul (a : i)) && FromFree b)
   ~> (FromFree (Mul (a : i)) && FromFree b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b

fromFree :: (BiCCC k) => Free (i :: [FK k]) a -> FromFree (Mul i) ~> FromFree a
fromFree :: forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree (Id @a) = forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
FromFree (Mul (b : i)) ~> FromFree b
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
FromFree (Mul (b : i)) ~> FromFree b
head @'[] @a
fromFree (L a ~> b
f Free i ('F a)
g) = a ~> b
f (a ~> b) -> (FromFree (Mul i) ~> a) -> FromFree (Mul i) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Free i ('F a) -> FromFree (Mul i) ~> FromFree ('F a)
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i ('F a)
g
fromFree (Head @a @_ @i Free '[a] a
f) = Free '[a] a -> FromFree (Mul '[a]) ~> FromFree a
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free '[a] a
f (FromFree a ~> FromFree a)
-> (FromFree (Mul (a : i)) ~> FromFree a)
-> FromFree (Mul (a : i)) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
FromFree (Mul (b : i)) ~> FromFree b
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
FromFree (Mul (b : i)) ~> FromFree b
head @i @a
fromFree (Tail @a @_ @i Free i a
f) = Free i a -> FromFree (Mul i) ~> FromFree a
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i a
f (FromFree (Mul i) ~> FromFree a)
-> (FromFree (Mul (a : i)) ~> FromFree (Mul i))
-> FromFree (Mul (a : i)) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
FromFree (Mul (b : i)) ~> FromFree (Mul i)
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
FromFree (Mul (b : i)) ~> FromFree (Mul i)
tail @i @a
fromFree (Ini @a Free i InitF
f) = forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @(FromFree a) (InitialObject ~> FromFree a)
-> (FromFree (Mul i) ~> InitialObject)
-> FromFree (Mul i) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Free i InitF -> FromFree (Mul i) ~> FromFree InitF
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i InitF
f ((Ob (FromFree a), Ob (FromFree a)) =>
 FromFree (Mul i) ~> FromFree a)
-> (FromFree a ~> FromFree a) -> FromFree (Mul i) ~> FromFree a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a
fromFree (Ter @i) = (FromFree (Mul i) ~> FromFree (Mul i))
-> FromFree (Mul i) ~> TerminalObject
forall {k} (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
terminate' (forall (i :: [FK k]). IsFKs i => Obj (FromFree (Mul i))
forall {k} (i :: [FK k]). IsFKs i => Obj (FromFree (Mul i))
fromFreeObjs @i)
fromFree (Lft @a @b Free i a
f) = (FromFree a ~> FromFree a)
-> Obj (FromFree b) -> FromFree a ~> (FromFree a || FromFree b)
forall {k} (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b) (FromFree a ~> (FromFree a || FromFree b))
-> (FromFree (Mul i) ~> FromFree a)
-> FromFree (Mul i) ~> (FromFree a || FromFree b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Free i a -> FromFree (Mul i) ~> FromFree a
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i a
f
fromFree (Rgt @a @b Free i b
f) = Obj (FromFree a)
-> (FromFree b ~> FromFree b)
-> FromFree b ~> (FromFree a || FromFree b)
forall {k} (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b) (FromFree b ~> (FromFree a || FromFree b))
-> (FromFree (Mul i) ~> FromFree b)
-> FromFree (Mul i) ~> (FromFree a || FromFree b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Free i b -> FromFree (Mul i) ~> FromFree b
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i b
f
fromFree (Sum @a @b @_ @i Free i (a + b)
m Free (a : i) a
f Free (b : i) a
g) =
  let ff :: FromFree (Mul (a : i)) ~> FromFree a
ff = Free (a : i) a -> FromFree (Mul (a : i)) ~> FromFree a
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free (a : i) a
f; fg :: FromFree (Mul (b : i)) ~> FromFree a
fg = Free (b : i) a -> FromFree (Mul (b : i)) ~> FromFree a
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free (b : i) a
g; fi :: FromFree (Mul i) ~> FromFree (Mul i)
fi = forall (i :: [FK k]). IsFKs i => Obj (FromFree (Mul i))
forall {k} (i :: [FK k]). IsFKs i => Obj (FromFree (Mul i))
fromFreeObjs @i
  in ( (FromFree (Mul (a : i)) ~> FromFree a
ff (FromFree (Mul (a : i)) ~> FromFree a)
-> ((FromFree (Mul i) && FromFree a) ~> FromFree (Mul (a : i)))
-> (FromFree (Mul i) && FromFree a) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
(FromFree (Mul i) && FromFree b) ~> FromFree (Mul (b : i))
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
(FromFree (Mul i) && FromFree b) ~> FromFree (Mul (b : i))
snoc @i @a ((FromFree (Mul i) && FromFree a) ~> FromFree a)
-> ((FromFree (Mul i) && FromFree b) ~> FromFree a)
-> ((FromFree (Mul i) && FromFree a)
    || (FromFree (Mul i) && FromFree b))
   ~> FromFree a
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FromFree (Mul (b : i)) ~> FromFree a
fg (FromFree (Mul (b : i)) ~> FromFree a)
-> ((FromFree (Mul i) && FromFree b) ~> FromFree (Mul (b : i)))
-> (FromFree (Mul i) && FromFree b) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
(FromFree (Mul i) && FromFree b) ~> FromFree (Mul (b : i))
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
(FromFree (Mul i) && FromFree b) ~> FromFree (Mul (b : i))
snoc @i @b) (((FromFree (Mul i) && FromFree a)
  || (FromFree (Mul i) && FromFree b))
 ~> FromFree a)
-> (FromFree (Mul i)
    ~> ((FromFree (Mul i) && FromFree a)
        || (FromFree (Mul i) && FromFree b)))
-> FromFree (Mul i) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd @(FromFree (Mul i)) @(FromFree a) @(FromFree b) ((FromFree (Mul i) && (FromFree a || FromFree b))
 ~> ((FromFree (Mul i) && FromFree a)
     || (FromFree (Mul i) && FromFree b)))
-> (FromFree (Mul i)
    ~> (FromFree (Mul i) && (FromFree a || FromFree b)))
-> FromFree (Mul i)
   ~> ((FromFree (Mul i) && FromFree a)
       || (FromFree (Mul i) && FromFree b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (FromFree (Mul i) ~> FromFree (Mul i)
fi (FromFree (Mul i) ~> FromFree (Mul i))
-> (FromFree (Mul i) ~> (FromFree a || FromFree b))
-> FromFree (Mul i)
   ~> (FromFree (Mul i) && (FromFree a || FromFree b))
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Free i (a + b) -> FromFree (Mul i) ~> FromFree (a + b)
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i (a + b)
m)
     )
      ((Ob (FromFree (Mul i)), Ob (FromFree (Mul i))) =>
 FromFree (Mul i) ~> FromFree a)
-> (FromFree (Mul i) ~> FromFree (Mul i))
-> FromFree (Mul i) ~> FromFree a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ FromFree (Mul i) ~> FromFree (Mul i)
fi
      ((Ob (FromFree a), Ob (FromFree a)) =>
 FromFree (Mul i) ~> FromFree a)
-> (FromFree a ~> FromFree a) -> FromFree (Mul i) ~> FromFree a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a
      ((Ob (FromFree b), Ob (FromFree b)) =>
 FromFree (Mul i) ~> FromFree a)
-> (FromFree b ~> FromFree b) -> FromFree (Mul i) ~> FromFree a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
fromFree (Fst @a @b Free i (a *! b)
f) = (FromFree a ~> FromFree a)
-> Obj (FromFree b) -> (FromFree a && FromFree b) ~> FromFree a
forall {k} (a :: k) (a' :: k) (b :: k).
HasBinaryProducts k =>
(a ~> a') -> Obj b -> (a && b) ~> a'
fst' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b) ((FromFree a && FromFree b) ~> FromFree a)
-> (FromFree (Mul i) ~> (FromFree a && FromFree b))
-> FromFree (Mul i) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Free i (a *! b) -> FromFree (Mul i) ~> FromFree (a *! b)
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i (a *! b)
f
fromFree (Snd @a @b Free i (a *! a)
f) = Obj (FromFree a)
-> (FromFree a ~> FromFree a)
-> (FromFree a && FromFree a) ~> FromFree a
forall {k} (a :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
Obj a -> (b ~> b') -> (a && b) ~> b'
snd' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b) ((FromFree a && FromFree a) ~> FromFree a)
-> (FromFree (Mul i) ~> (FromFree a && FromFree a))
-> FromFree (Mul i) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Free i (a *! a) -> FromFree (Mul i) ~> FromFree (a *! a)
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i (a *! a)
f
fromFree (Prd Free i a
f Free i b
g) = Free i a -> FromFree (Mul i) ~> FromFree a
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i a
f (FromFree (Mul i) ~> FromFree a)
-> (FromFree (Mul i) ~> FromFree b)
-> FromFree (Mul i) ~> (FromFree a && FromFree b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Free i b -> FromFree (Mul i) ~> FromFree b
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i b
g
fromFree (Curry @a @b @i Free (a : i) b
f) =
  forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @(FromFree (Mul i)) @(FromFree a) @(FromFree b) (Free (a : i) b -> FromFree (Mul (a : i)) ~> FromFree b
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free (a : i) b
f (FromFree (Mul (a : i)) ~> FromFree b)
-> ((FromFree (Mul i) ** FromFree a) ~> FromFree (Mul (a : i)))
-> (FromFree (Mul i) ** FromFree a) ~> FromFree b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
(FromFree (Mul i) && FromFree b) ~> FromFree (Mul (b : i))
forall {k} (i :: [FK k]) (b :: FK k).
(IsFKs i, IsFK b) =>
(FromFree (Mul i) && FromFree b) ~> FromFree (Mul (b : i))
snoc @i @a) ((Ob (FromFree a), Ob (FromFree a)) =>
 FromFree (Mul i) ~> (FromFree a ~~> FromFree b))
-> (FromFree a ~> FromFree a)
-> FromFree (Mul i) ~> (FromFree a ~~> FromFree b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a ((Ob (FromFree (Mul i)), Ob (FromFree (Mul i))) =>
 FromFree (Mul i) ~> (FromFree a ~~> FromFree b))
-> (FromFree (Mul i) ~> FromFree (Mul i))
-> FromFree (Mul i) ~> (FromFree a ~~> FromFree b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall (i :: [FK k]). IsFKs i => Obj (FromFree (Mul i))
forall {k} (i :: [FK k]). IsFKs i => Obj (FromFree (Mul i))
fromFreeObjs @i
fromFree (Apply @a @b Free i (a --> a)
f Free i a
g) = forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @(FromFree a) @(FromFree b) (((FromFree a ~~> FromFree a) ** FromFree a) ~> FromFree a)
-> (FromFree (Mul i)
    ~> ((FromFree a ~~> FromFree a) ** FromFree a))
-> FromFree (Mul i) ~> FromFree a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Free i (a --> a) -> FromFree (Mul i) ~> FromFree (a --> a)
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i (a --> a)
f (FromFree (Mul i) ~> (FromFree a ~~> FromFree a))
-> (FromFree (Mul i) ~> FromFree a)
-> FromFree (Mul i) ~> ((FromFree a ~~> FromFree a) && FromFree a)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Free i a -> FromFree (Mul i) ~> FromFree a
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree Free i a
g) ((Ob (FromFree a), Ob (FromFree a)) =>
 FromFree (Mul i) ~> FromFree a)
-> (FromFree a ~> FromFree a) -> FromFree (Mul i) ~> FromFree a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a ((Ob (FromFree a), Ob (FromFree a)) =>
 FromFree (Mul i) ~> FromFree a)
-> (FromFree a ~> FromFree a) -> FromFree (Mul i) ~> FromFree a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b

type IsFK :: forall {k}. FK k -> Constraint
class IsFK (a :: FK k) where
  fromFreeObj :: Obj (FromFree a)
instance (CategoryOf k, Ob a) => IsFK (F (a :: k)) where
  fromFreeObj :: Obj (FromFree ('F a))
fromFreeObj = a ~> a
Obj (FromFree ('F a))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (HasInitialObject k) => IsFK (InitF :: FK k) where
  fromFreeObj :: Obj (FromFree InitF)
fromFreeObj = Obj InitialObject
Obj (FromFree InitF)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
instance (HasTerminalObject k) => IsFK (TermF :: FK k) where
  fromFreeObj :: Obj (FromFree TermF)
fromFreeObj = Obj TerminalObject
Obj (FromFree TermF)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
instance (HasBinaryCoproducts k, IsFK a, IsFK b) => IsFK (a + b :: FK k) where
  fromFreeObj :: Obj (FromFree (a + b))
fromFreeObj = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a Obj (FromFree a)
-> (FromFree b ~> FromFree b)
-> (FromFree a || FromFree b) ~> (FromFree a || FromFree b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
instance (HasBinaryProducts k, IsFK a, IsFK b) => IsFK (a *! b :: FK k) where
  fromFreeObj :: Obj (FromFree (a *! b))
fromFreeObj = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a Obj (FromFree a)
-> (FromFree b ~> FromFree b)
-> (FromFree a && FromFree b) ~> (FromFree a && FromFree b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
instance (Closed k, IsFK a, IsFK b) => IsFK (a --> b :: FK k) where
  fromFreeObj :: Obj (FromFree (a --> b))
fromFreeObj = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b Obj (FromFree b)
-> (FromFree a ~> FromFree a)
-> (FromFree a ~~> FromFree b) ~> (FromFree a ~~> FromFree b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a

-- | Adapted from Phil Freeman: https://blog.functorial.com/posts/2017-10-08-HOAS-CCCs.html
toCCC :: forall {k} a b. (BiCCC k) => (IsFK (a :: FK k), IsFK b) => (Free '[] (a --> b)) -> FromFree a ~> FromFree b
toCCC :: forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, IsFK a, IsFK b) =>
Free '[] (a --> b) -> FromFree a ~> FromFree b
toCCC Free '[] (a --> b)
f = Free '[a] b -> FromFree (Mul '[a]) ~> FromFree b
forall k (i :: [FK k]) (a :: FK k).
BiCCC k =>
Free i a -> FromFree (Mul i) ~> FromFree a
fromFree (Free '[] (a --> b) -> Free '[a] b
forall k (a :: FK k) (b :: FK k) (i :: [FK k]).
(IsFK a, IsFK b, IsFKs i, Closed k) =>
Free i (a --> b) -> Free (a : i) b
Uncurry Free '[] (a --> b)
f)

-- debug :: (IsFK a, IsFK b) => Free '[] ((a :: FK ()) --> b) -> P.String
-- debug f = P.show (Uncurry f)

-- test1 :: forall {k} (a :: k) b. (BiCCC k, Ob (a :: k), Ob b) => a ~> b || a
-- test1 = toCCC @(F a) @(F b + F a) (lam \x -> Rgt x)
-- test2 :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => a && b ~> b && a
-- test2 = toCCC @(F a *! F b) @(F b *! F a) (lam \(x :& y) -> (y :& x))
-- test3 :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => (a ~~> b) && a ~> b
-- test3 = toCCC @((F a --> F b) *! F a) @(F b) (lam \(f :& a) -> f $ a)
-- test4 :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => a ~> b ~~> (a && b)
-- test4 = toCCC @(F a) @(F b --> F a *! F b) (lam \x -> lam \y -> (x :& y))
-- test5 :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => (a && b) ~> (b && a)
-- test5 = toCCC @(F a *! F b) @(F b *! F a) (lam \(a :& b) -> lam (\c -> (b :& c)) $ a)
-- test6 :: forall {k} a b c. (BiCCC k, Ob (a :: k), Ob b, Ob c) => b ~~> a ~~> b ~~> c ~> a ~~> b ~~> c
-- test6 = toCCC @(F b --> F a --> F b --> F c) @(F a --> F b --> F c) (lam (\x -> lam (\y -> lam (\z -> ((x $ z) $ y) $ z))))
-- test7 :: forall {k} a b. (BiCCC k, Ob (a :: k), Ob b) => (a || b) ~> (b || a)
-- test7 = toCCC @(F a + F b) @(F b + F a) (lam \x -> either (lam \y -> Rgt y) (lam \y -> Lft y) x)
-- test8 :: forall {k} (a :: k) b c. (BiCCC k, Ob a, Ob b, Ob c) => a && (b || c) ~> (a && b) || (a && c)
-- test8 =
--   toCCC @(F a *! (F b + F c)) @((F a *! F b) + (F a *! F c))
--     (lam \(a :& bc) -> either (lam \b -> Lft (Tail a :& b)) (lam \c -> Rgt (Tail a :& c)) bc)