{-# LANGUAGE AllowAmbiguousTypes #-}

{- HLINT ignore "Redundant $" -}

-- | A small HOAS (higher-order abstract syntax) front end for building morphisms in any
-- 'BiCCC', compiling through the free category of "Proarrow.Category.Instance.Free" with the
-- bicartesian closed structures rather than a bespoke one. A 'Free' term tracks its free
-- variables via a context list, the way a well-scoped lambda calculus does; 'lam' binds an
-- ordinary Haskell-level variable that 'Cast' automatically "weakens" across nested lambdas so
-- inner lambdas can still refer to outer ones. 'toCCC' interprets a closed term (no free
-- variables) into an actual morphism of the target category.
module Proarrow.Tools.CCC
  ( toCCC
  , lam
  , ($)
  , lift
  , pattern (:&)
  , either
  , lft
  , rgt
  , Free
  , Syntax
  , Ctx
  , Mul
  , Cast (..)
  , KnownCtx (..)
  , BiCCCStructs
  , type F
  , injectRight
  , swapProduct
  , applyPair
  , curryPair
  , flipCurried3
  , swapSum
  , caseEither
  ) where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Category.Instance.Free (FREE (..), Lower, emb, fold)
import Proarrow.Category.Monoidal (Monoidal)
import Proarrow.Category.Monoidal.Cartesian (BiCCC, Cartesian, prodToTensor, tensorToProd, unitToTerm)
import Proarrow.Category.Monoidal.Closed (Closed (..), lower)
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts ((+++), (|||)), type (||))
import Proarrow.Colimit.BinaryCoproduct qualified as BC
import Proarrow.Colimit.Initial (HasInitialObject)
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), type (*!))
import Proarrow.Limit.Terminal (HasTerminalObject, TermF)
import Proarrow.Object (Obj)
import Proarrow.Profunctor.Instance.Identity (Id (..))

infixr 0 $

-- | The structures of a bicartesian closed category as a list for 'FREE': the five BiCCC
-- classes, the 'Cartesian' marker supplying the formal @tensor = product@ coercions (the free
-- category cannot state that type equality itself), and 'Distributive', for case analysis in the
-- presence of a context.
type BiCCCStructs =
  '[ HasTerminalObject
   , HasInitialObject
   , HasBinaryProducts
   , HasBinaryCoproducts
   , Monoidal
   , Closed
   , Cartesian
   , Distributive
   ]

-- | The syntax category over @k@: the free BiCCC on @k@'s own hom-sets, i.e. 'Id'. @(~>)@ itself
-- is an unsaturated type family application, so it isn't allowed as a type index where it is
-- pattern-matched on below, in 'Mul'.
type Syntax k = FREE BiCCCStructs (Id :: CAT k)

type Ctx k = [Syntax k]

-- | A short alias for embedding a base-category object, so type applications built from it read
-- like the target signature: '&&', '||' and '~~>' on the free category are its object formers,
-- so @(F a ~~> F b) && F a@ is the object it looks like.
type F a = EMB a

-- | The context product: @'Mul' i@ is the single object standing in for "all the bound
-- variables in @i@", a right fold with the most-recently-bound variable last. This mirrors
-- "Proarrow.Category.Monoidal.Strictified"'s @Fold@, which puts its head leftmost. @Fold@ itself
-- can't be reused, since 'curry'\/'fst'\/'snd' expect the thing being abstracted over on the right
-- of the product.
type family Mul (i :: Ctx k) :: Syntax k where
  Mul '[] = TermF
  Mul (a ': as) = Mul as *! a

-- | A term with free variables @i@ (innermost\/most-recently-bound first) and result type
-- @a@: a morphism from the context product to @a@ in the free BiCCC. A newtype
-- (rather than a bare type synonym) so that @i@ is recoverable from a 'Free' term's type: 'Mul'
-- is many-to-one at the type-family level as far as GHC's injectivity checker is concerned (even
-- though it's mathematically injective here), which would otherwise leave @i@ ambiguous wherever
-- it has to be inferred rather than given explicitly (e.g. picking which context a HOAS variable
-- reference in 'lam' denotes).
newtype Free (i :: Ctx k) (a :: Syntax k) = MkFree {forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree :: Mul i ~> a}

type KnownCtx :: forall {k}. Ctx k -> Constraint
class KnownCtx (i :: Ctx k) where
  ctxOb :: Obj (Mul i)

instance KnownCtx ('[] :: Ctx k) where
  ctxOb :: Obj (Mul '[])
ctxOb = Obj (Mul '[])
Free TermF TermF
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Syntax k). Ob a => Free a a
id

instance (KnownCtx i, Ob (b :: Syntax k)) => KnownCtx (b ': i) where
  ctxOb :: Obj (Mul (b : i))
ctxOb = Free (Mul i *! b) (Mul i *! b)
(Ob (Mul i), Ob (Mul i)) => Free (Mul i *! b) (Mul i *! b)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Syntax k). Ob a => Free a a
id ((Ob (Mul i), Ob (Mul i)) => Free (Mul i *! b) (Mul i *! b))
-> Free (Mul i) (Mul i) -> Free (Mul i *! b) (Mul i *! b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Syntax k) (b :: Syntax k) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ forall (i :: Ctx k). KnownCtx i => Obj (Mul i)
forall {k} (i :: Ctx k). KnownCtx i => Obj (Mul i)
ctxOb @i

-- | The most-recently-bound variable.
headT :: forall {k} a i. (KnownCtx (i :: Ctx k), Ob (a :: Syntax k)) => Free (a ': i) a
headT :: forall {k} (a :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a) =>
Free (a : i) a
headT = (Mul (a : i) ~> a) -> Free (a : i) a
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @(Syntax k) @(Mul i) @a) ((Ob (Mul i), Ob (Mul i)) => Free (a : i) a)
-> Free (Mul i) (Mul i) -> Free (a : i) a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Syntax k) (b :: Syntax k) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ forall (i :: Ctx k). KnownCtx i => Obj (Mul i)
forall {k} (i :: Ctx k). KnownCtx i => Obj (Mul i)
ctxOb @i

-- | Weaken a term by one more bound variable it doesn't use.
tailT :: forall {k} a i b. (KnownCtx (i :: Ctx k), Ob (a :: Syntax k)) => Free i b -> Free (a ': i) b
tailT :: forall {k} (a :: Syntax k) (i :: Ctx k) (b :: Syntax k).
(KnownCtx i, Ob a) =>
Free i b -> Free (a : i) b
tailT (MkFree Mul i ~> b
f) = (Mul (a : i) ~> b) -> Free (a : i) b
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (Mul i ~> b
Free (Mul i) b
f Free (Mul i) b -> Free (Mul i *! a) (Mul i) -> Free (Mul i *! a) b
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @(Syntax k) @(Mul i) @a) ((Ob (Mul i), Ob (Mul i)) => Free (a : i) b)
-> Free (Mul i) (Mul i) -> Free (a : i) b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Syntax k) (b :: Syntax k) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ forall (i :: Ctx k). KnownCtx i => Obj (Mul i)
forall {k} (i :: Ctx k). KnownCtx i => Obj (Mul i)
ctxOb @i

-- | @'Cast' i j@ holds when context @i@ is context @j@ with zero or more extra variables
-- pushed on top, letting a term built for @j@ be used anywhere \"deeper\" than @j@.
type Cast :: forall {k}. Ctx k -> Ctx k -> Constraint
class Cast (i :: Ctx k) (j :: Ctx k) where
  cast :: (Ob (a :: Syntax k)) => Free j a -> Free i a

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

instance
  {-# OVERLAPPABLE #-}
  (Cast i j, KnownCtx (i :: Ctx k), Ob (b :: Syntax k), (b ': i) ~ i')
  => Cast i' j
  where
  cast :: forall (a :: Syntax k). Ob a => Free j a -> Free i' a
cast Free j a
f = Free i a -> Free (b : i) a
forall {k} (a :: Syntax k) (i :: Ctx k) (b :: Syntax k).
(KnownCtx i, Ob a) =>
Free i b -> Free (a : i) b
tailT (Free j a -> Free i a
forall {k} (i :: Ctx k) (j :: Ctx k) (a :: Syntax k).
(Cast i j, Ob a) =>
Free j a -> Free i a
forall (a :: Syntax k). Ob a => Free j a -> Free i a
cast Free j a
f)

-- | Bind a variable, HOAS-style: the function argument stands for the newly bound variable,
-- usable (via 'Cast') in the body of this 'lam' and any 'lam' nested inside it. The body is a
-- morphism out of the context product, but 'curry' wants the tensor, so the 'Cartesian'
-- coercion mediates.
lam
  :: forall {k} a b i
   . (KnownCtx (i :: Ctx k), Ob (a :: Syntax k), Ob b)
  => ((forall (x :: Ctx k). (Cast x (a ': i)) => Free x a) -> Free (a ': i) b)
  -> Free i (a ~~> b)
lam :: forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (forall (x :: Ctx k). Cast x (a : i) => Free x a) -> Free (a : i) b
f = (Mul i ~> (a --> b)) -> Free i (a --> b)
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @(Syntax k) @(Mul i) @a @b (Free (a : i) b -> Mul (a : i) ~> b
forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree ((forall (x :: Ctx k). Cast x (a : i) => Free x a) -> Free (a : i) b
f Free x a
forall (x :: Ctx k). Cast x (a : i) => Free x a
xa) Free (Mul i *! a) b
-> Free (Mul i **! a) (Mul i *! a) -> Free (Mul i **! a) b
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal] cs,
 Ob a, Ob b) =>
(a **! b) ~> (a *! b)
forall (a :: Syntax k) (b :: Syntax k).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal]
   '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
     HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive],
 Ob a, Ob b) =>
(a **! b) ~> (a *! b)
tensorToProd @(Mul i) @a)) ((Ob (Mul i), Ob (Mul i)) => Free i (a --> b))
-> Free (Mul i) (Mul i) -> Free i (a --> b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Syntax k) (b :: Syntax k) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ forall (i :: Ctx k). KnownCtx i => Obj (Mul i)
forall {k} (i :: Ctx k). KnownCtx i => Obj (Mul i)
ctxOb @i
  where
    xa :: forall (x :: Ctx k). (Cast x (a ': i)) => Free x a
    xa :: forall (x :: Ctx k). Cast x (a : i) => Free x a
xa = Free (a : i) a -> Free x a
forall {k} (i :: Ctx k) (j :: Ctx k) (a :: Syntax k).
(Cast i j, Ob a) =>
Free j a -> Free i a
forall (a :: Syntax k). Ob a => Free (a : i) a -> Free x a
cast (forall {k} (a :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a) =>
Free (a : i) a
forall (a :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a) =>
Free (a : i) a
headT @a @i)

-- | Function application.
($) :: forall {k} a b i. (Ob (a :: Syntax k), Ob b) => Free i (a ~~> b) -> Free i a -> Free i b
MkFree Mul i ~> (a ~~> b)
f $ :: forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i (a ~~> b) -> Free i a -> Free i b
$ MkFree Mul i ~> a
g = (Mul i ~> b) -> Free i b
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @(Syntax k) @a @b Free ((a --> b) **! a) b
-> Free (Mul i) ((a --> b) **! a) -> Free (Mul i) b
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal] cs,
 Ob a, Ob b) =>
(a *! b) ~> (a **! b)
forall (a :: Syntax k) (b :: Syntax k).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal]
   '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
     HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive],
 Ob a, Ob b) =>
(a *! b) ~> (a **! b)
prodToTensor @(a ~~> b) @a Free ((a --> b) *! a) ((a --> b) **! a)
-> Free (Mul i) ((a --> b) *! a) -> Free (Mul i) ((a --> b) **! a)
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. (Mul i ~> (a --> b)
Mul i ~> (a ~~> b)
f (Mul i ~> (a --> b)) -> (Mul i ~> a) -> Mul i ~> ((a --> b) && a)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: Syntax k) (x :: Syntax k) (y :: Syntax k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Mul i ~> a
g))

-- | Embed a morphism of the target category as a term between embedded objects.
lift :: forall {k} a b i. (Ob (a :: k), Ob b) => a ~> b -> Free i (F a) -> Free i (F b)
lift :: forall {k} (a :: k) (b :: k) (i :: Ctx k).
(Ob a, Ob b) =>
(a ~> b) -> Free i (F a) -> Free i (F b)
lift a ~> b
f (MkFree Mul i ~> F a
g) = (Mul i ~> F b) -> Free i (F b)
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (Id a b %1 -> Free (F a) (F b)
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (cs :: [Type -> Constraint]).
(Ob a, Ob b) =>
p a b %1 -> Free (EMB a) (EMB b)
emb ((a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> b
f) Free (F a) (F b) -> Free (Mul i) (F a) -> Free (Mul i) (F b)
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE
               '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
                 HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive]
               Id)
       (c :: FREE
               '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
                 HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive]
               Id)
       (a :: FREE
               '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
                 HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive]
               Id).
Free b c -> Free a b -> Free a c
. Mul i ~> F a
Free (Mul i) (F a)
g)

fstSnd :: forall {k} a b i. (Ob (a :: Syntax k), Ob b) => Free i (a && b) -> (Free i a, Free i b)
fstSnd :: forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i (a && b) -> (Free i a, Free i b)
fstSnd (MkFree Mul i ~> (a && b)
f) = ((Mul i ~> a) -> Free i a
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @(Syntax k) @a @b Free (a *! b) a -> Free (Mul i) (a *! b) -> Free (Mul i) a
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. Mul i ~> (a && b)
Free (Mul i) (a *! b)
f), (Mul i ~> b) -> Free i b
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @(Syntax k) @a @b Free (a *! b) b -> Free (Mul i) (a *! b) -> Free (Mul i) b
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. Mul i ~> (a && b)
Free (Mul i) (a *! b)
f))

pattern (:&) :: (Ob (a :: Syntax k), Ob b) => Free i a -> Free i b -> Free i (a && b)
pattern x $b:& :: forall k (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i a -> Free i b -> Free i (a && b)
$m:& :: forall {r} {k} {a :: Syntax k} {b :: Syntax k} {i :: Ctx k}.
(Ob a, Ob b) =>
Free i (a && b) -> (Free i a -> Free i b -> r) -> ((# #) -> r) -> r
:& y <- (fstSnd -> (x, y))
  where
    Free i a
x :& Free i b
y = (Mul i ~> (a *! b)) -> Free i (a *! b)
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (Free i a -> Mul i ~> a
forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree Free i a
x (Mul i ~> a) -> (Mul i ~> b) -> Mul i ~> (a && b)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: Syntax k) (x :: Syntax k) (y :: Syntax k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Free i b -> Mul i ~> b
forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree Free i b
y)

{-# COMPLETE (:&) #-}

-- | Inject as the left\/right branch of a sum.
lft :: forall {k} a b i. (Ob (a :: Syntax k), Ob b) => Free i a -> Free i (a || b)
lft :: forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i a -> Free i (a || b)
lft (MkFree Mul i ~> a
f) = (Mul i ~> (a + b)) -> Free i (a + b)
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
BC.lft @(Syntax k) @a @b Free a (a + b) -> Free (Mul i) a -> Free (Mul i) (a + b)
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. Mul i ~> a
Free (Mul i) a
f)

rgt :: forall {k} a b i. (Ob (a :: Syntax k), Ob b) => Free i b -> Free i (a || b)
rgt :: forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i b -> Free i (a || b)
rgt (MkFree Mul i ~> b
f) = (Mul i ~> (a + b)) -> Free i (a + b)
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
BC.rgt @(Syntax k) @a @b Free b (a + b) -> Free (Mul i) b -> Free (Mul i) (a + b)
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. Mul i ~> b
Free (Mul i) b
f)

-- | Uncurry a function term into the body of a 'lam' binding its argument.
uncurryF
  :: forall {k} a b i
   . (KnownCtx (i :: Ctx k), Ob (a :: Syntax k), Ob b)
  => Free i (a ~~> b) -> Free (a ': i) b
uncurryF :: forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
Free i (a ~~> b) -> Free (a : i) b
uncurryF Free i (a ~~> b)
f = (Mul (a : i) ~> b) -> Free (a : i) b
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @(Syntax k) @a @b Free ((a --> b) **! a) b
-> Free (Mul i *! a) ((a --> b) **! a) -> Free (Mul i *! a) b
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal] cs,
 Ob a, Ob b) =>
(a *! b) ~> (a **! b)
forall (a :: Syntax k) (b :: Syntax k).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal]
   '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
     HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive],
 Ob a, Ob b) =>
(a *! b) ~> (a **! b)
prodToTensor @(a ~~> b) @a Free ((a --> b) *! a) ((a --> b) **! a)
-> Free (Mul i *! a) ((a --> b) *! a)
-> Free (Mul i *! a) ((a --> b) **! a)
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. (Free (a : i) (a --> b) -> Mul (a : i) ~> (a --> b)
forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree (Free i (a --> b) -> Free (a : i) (a --> b)
forall {k} (a :: Syntax k) (i :: Ctx k) (b :: Syntax k).
(KnownCtx i, Ob a) =>
Free i b -> Free (a : i) b
tailT Free i (a --> b)
Free i (a ~~> b)
f) ((Mul i *! a) ~> (a --> b))
-> ((Mul i *! a) ~> a) -> (Mul i *! a) ~> ((a --> b) && a)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: Syntax k) (x :: Syntax k) (y :: Syntax k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Free (a : i) a -> Mul (a : i) ~> a
forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree (forall {k} (a :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a) =>
Free (a : i) a
forall (a :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a) =>
Free (a : i) a
headT @a @i)))

-- | Case analysis on a sum, in the presence of a shared context: distributes the context over
-- the sum, so each branch still has access to it. The free category's distributivity is stated
-- for the tensor, so the product is coerced to the tensor and back around 'distL'.
caseT
  :: forall {k} a b c i
   . (KnownCtx (i :: Ctx k), Ob (a :: Syntax k), Ob b)
  => Free i (a || b) -> Free (a ': i) c -> Free (b ': i) c -> Free i c
caseT :: forall {k} (a :: Syntax k) (b :: Syntax k) (c :: Syntax k)
       (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
Free i (a || b) -> Free (a : i) c -> Free (b : i) c -> Free i c
caseT Free i (a || b)
m Free (a : i) c
f Free (b : i) c
g =
  (Mul i ~> c) -> Free i c
forall k (i :: Ctx k) (a :: Syntax k). (Mul i ~> a) -> Free i a
MkFree
    ( (Free (a : i) c -> Mul (a : i) ~> c
forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree Free (a : i) c
f ((Mul i *! a) ~> c)
-> ((Mul i *! b) ~> c) -> ((Mul i *! a) || (Mul i *! b)) ~> c
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: Syntax k) (a :: Syntax k) (y :: Syntax k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Free (b : i) c -> Mul (b : i) ~> c
forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree Free (b : i) c
g)
        Free ((Mul i *! a) + (Mul i *! b)) c
-> Free (Mul i) ((Mul i *! a) + (Mul i *! b)) -> Free (Mul i) c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. (forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal] cs,
 Ob a, Ob b) =>
(a **! b) ~> (a *! b)
forall (a :: Syntax k) (b :: Syntax k).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal]
   '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
     HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive],
 Ob a, Ob b) =>
(a **! b) ~> (a *! b)
tensorToProd @(Mul i) @a ((Mul i **! a) ~> (Mul i *! a))
-> ((Mul i **! b) ~> (Mul i *! b))
-> ((Mul i **! a) || (Mul i **! b))
   ~> ((Mul i *! a) || (Mul i *! b))
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall (a :: Syntax k) (b :: Syntax k) (x :: Syntax k)
       (y :: Syntax k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal] cs,
 Ob a, Ob b) =>
(a **! b) ~> (a *! b)
forall (a :: Syntax k) (b :: Syntax k).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal]
   '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
     HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive],
 Ob a, Ob b) =>
(a **! b) ~> (a *! b)
tensorToProd @(Mul i) @b)
        Free ((Mul i **! a) + (Mul i **! b)) ((Mul i *! a) + (Mul i *! b))
-> Free (Mul i) ((Mul i **! a) + (Mul i **! b))
-> Free (Mul i) ((Mul i *! a) + (Mul i *! b))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @(Syntax k) @(Mul i) @a @b
        Free (Mul i **! (a + b)) ((Mul i **! a) + (Mul i **! b))
-> Free (Mul i) (Mul i **! (a + b))
-> Free (Mul i) ((Mul i **! a) + (Mul i **! b))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal] cs,
 Ob a, Ob b) =>
(a *! b) ~> (a **! b)
forall (a :: Syntax k) (b :: Syntax k).
(Elems
   '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal]
   '[HasTerminalObject, HasInitialObject, HasBinaryProducts,
     HasBinaryCoproducts, Monoidal, Closed, Cartesian, Distributive],
 Ob a, Ob b) =>
(a *! b) ~> (a **! b)
prodToTensor @(Mul i) @(a || b)
        Free (Mul i *! (a + b)) (Mul i **! (a + b))
-> Free (Mul i) (Mul i *! (a + b))
-> Free (Mul i) (Mul i **! (a + b))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. (Mul i ~> Mul i
Free (Mul i) (Mul i)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Syntax k). Ob a => Free a a
id (Mul i ~> Mul i)
-> (Mul i ~> (a + b)) -> Mul i ~> (Mul i && (a + b))
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: Syntax k) (x :: Syntax k) (y :: Syntax k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Free i (a + b) -> Mul i ~> (a + b)
forall k (i :: Ctx k) (a :: Syntax k). Free i a -> Mul i ~> a
unFree Free i (a + b)
Free i (a || b)
m)
    )
    ((Ob (Mul i), Ob (Mul i)) => Free i c)
-> Free (Mul i) (Mul i) -> Free i c
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Syntax k) (b :: Syntax k) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ forall (i :: Ctx k). KnownCtx i => Obj (Mul i)
forall {k} (i :: Ctx k). KnownCtx i => Obj (Mul i)
ctxOb @i

either
  :: forall {k} a b c i
   . (KnownCtx (i :: Ctx k), Ob (a :: Syntax k), Ob b, Ob c)
  => Free i (a ~~> c) -> Free i (b ~~> c) -> Free i (a || b) -> Free i c
either :: forall {k} (a :: Syntax k) (b :: Syntax k) (c :: Syntax k)
       (i :: Ctx k).
(KnownCtx i, Ob a, Ob b, Ob c) =>
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 :: Syntax k) (b :: Syntax k) (c :: Syntax k)
       (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
Free i (a || b) -> Free (a : i) c -> Free (b : i) c -> Free i c
caseT Free i (a || b)
m (Free i (a ~~> c) -> Free (a : i) c
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
Free i (a ~~> b) -> Free (a : i) b
uncurryF Free i (a ~~> c)
f) (Free i (b ~~> c) -> Free (b : i) c
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
Free i (a ~~> b) -> Free (a : i) b
uncurryF Free i (b ~~> c)
g)

-- | Interpret a closed term (no free variables) into an actual morphism of the target
-- category: move the empty context from the terminal object to the monoidal unit, 'lower' the
-- function-valued term (a closed one needs no arguments to uncurry), and 'fold' into @k@ with
-- generators interpreted by unwrapping 'Id' (the free category was built over @k@'s own
-- hom-sets directly).
toCCC
  :: forall {k} a b
   . (BiCCC k, Ob (a :: Syntax k), Ob b)
  => Free '[] (a ~~> b) -> Lower (Id :: CAT k) a ~> Lower (Id :: CAT k) b
toCCC :: forall {k} (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
toCCC (MkFree Mul '[] ~> (a ~~> b)
f) = forall (cs :: [Type -> Constraint]) (f :: k +-> k)
       (a :: FREE cs Id) (b :: FREE cs Id).
(All cs k, Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 Id x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
forall {k} {k'} {p :: CAT k} (cs :: [Type -> Constraint])
       (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(All cs k', Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 p x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
fold @BiCCCStructs @(Id :: CAT k) Id x y -> x ~> y
Id x y -> (Id % x) ~> (Id % y)
forall (x :: k) (y :: k).
(Ob x, Ob y) =>
Id x y -> (Id % x) ~> (Id % y)
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId (forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
(Unit ~> (a ~~> b)) -> a ~> b
forall (a :: Syntax k) (b :: Syntax k).
(Closed (Syntax k), Ob a, Ob b) =>
(Unit ~> (a ~~> b)) -> a ~> b
lower @a @b (Mul '[] ~> (a ~~> b)
Free TermF (a --> b)
f Free TermF (a --> b) -> Free UnitF TermF -> Free UnitF (a --> b)
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Syntax k) (c :: Syntax k) (a :: Syntax k).
Free b c -> Free a b -> Free a c
. UnitF ~> TermF
Free UnitF TermF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}.
Elems
  '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal] cs =>
UnitF ~> TermF
unitToTerm))

-- $
-- The examples below exercise 'lam'\/'Cast' (including nested lambdas) and 'toCCC' at
-- @k = 'Type'@, where the compiled morphism can be run and its result printed.

-- | Inject as the right element of a sum.
--
-- >>> import Prelude (Bool (..))
-- >>> injectRight @Bool @Bool True
-- Right True
injectRight :: forall {k} (a :: k) b. (BiCCC k, Ob (a :: k), Ob b) => a ~> (b || a)
injectRight :: forall {k} (a :: k) (b :: k).
(BiCCC k, Ob a, Ob b) =>
a ~> (b || a)
injectRight = forall {k} (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
forall (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
toCCC @(F a) @(F b || F a) (((forall (x :: Ctx k). Cast x '[F a] => Free x (F a))
 -> Free '[F a] (F b + F a))
-> Free '[] (F a ~~> (F b + F a))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: Ctx k). Cast x '[F a] => Free x (F a)
x -> Free '[F a] (F a) -> Free '[F a] (F b || F a)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i b -> Free i (a || b)
rgt Free '[F a] (F a)
forall (x :: Ctx k). Cast x '[F a] => Free x (F a)
x))

-- | Swap a product.
--
-- >>> import Prelude (Bool (..))
-- >>> swapProduct @Bool @Bool (True, False)
-- (False,True)
swapProduct :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => (a && b) ~> (b && a)
swapProduct :: forall {k} (a :: k) (b :: k).
(BiCCC k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProduct = forall {k} (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
forall (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
toCCC @(F a && F b) @(F b && F a) (((forall (x :: Ctx k). Cast x '[F a *! F b] => Free x (F a *! F b))
 -> Free '[F a *! F b] (F b *! F a))
-> Free '[] ((F a *! F b) ~~> (F b *! F a))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: Ctx k). Cast x '[F a *! F b] => Free x (F a *! F b)
p -> let (Free '[F a *! F b] (F a)
x :& Free '[F a *! F b] (F b)
y) = Free '[F a *! F b] (F a *! F b)
forall (x :: Ctx k). Cast x '[F a *! F b] => Free x (F a *! F b)
p in Free '[F a *! F b] (F b)
y Free '[F a *! F b] (F b)
-> Free '[F a *! F b] (F a) -> Free '[F a *! F b] (F b && F a)
forall k (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i a -> Free i b -> Free i (a && b)
:& Free '[F a *! F b] (F a)
x))

-- | Apply a function to an argument, both bundled in a product.
--
-- >>> import Prelude (Bool (..), not)
-- >>> applyPair @Bool @Bool (not, True)
-- False
applyPair :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => ((a ~~> b) && a) ~> b
applyPair :: forall {k} (a :: k) (b :: k).
(BiCCC k, Ob a, Ob b) =>
((a ~~> b) && a) ~> b
applyPair = forall {k} (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
forall (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
toCCC @((F a ~~> F b) && F a) @(F b) (((forall (x :: Ctx k).
  Cast x '[(F a --> F b) *! F a] =>
  Free x ((F a --> F b) *! F a))
 -> Free '[(F a --> F b) *! F a] (F b))
-> Free '[] (((F a --> F b) *! F a) ~~> F b)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: Ctx k).
Cast x '[(F a --> F b) *! F a] =>
Free x ((F a --> F b) *! F a)
p -> let (Free '[(F a --> F b) *! F a] (F a --> F b)
f :& Free '[(F a --> F b) *! F a] (F a)
a) = Free '[(F a --> F b) *! F a] ((F a --> F b) *! F a)
forall (x :: Ctx k).
Cast x '[(F a --> F b) *! F a] =>
Free x ((F a --> F b) *! F a)
p in Free '[(F a --> F b) *! F a] (F a --> F b)
Free '[(F a --> F b) *! F a] (F a ~~> F b)
f Free '[(F a --> F b) *! F a] (F a ~~> F b)
-> Free '[(F a --> F b) *! F a] (F a)
-> Free '[(F a --> F b) *! F a] (F b)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i (a ~~> b) -> Free i a -> Free i b
$ Free '[(F a --> F b) *! F a] (F a)
a))

-- | Curry a pairing function.
--
-- >>> import Prelude (Bool (..))
-- >>> curryPair @Bool @Bool True False
-- (True,False)
curryPair :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => a ~> (b ~~> (a && b))
curryPair :: forall {k} (a :: k) (b :: k).
(BiCCC k, Ob a, Ob b) =>
a ~> (b ~~> (a && b))
curryPair = forall {k} (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
forall (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
toCCC @(F a) @(F b ~~> (F a && F b)) (((forall (x :: [Syntax k]). Cast x '[F a] => Free x (F a))
 -> Free '[F a] (F b --> (F a *! F b)))
-> Free '[] (F a ~~> (F b --> (F a *! F b)))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: [Syntax k]). Cast x '[F a] => Free x (F a)
x -> ((forall (x :: [Syntax k]). Cast x '[F b, F a] => Free x (F b))
 -> Free '[F b, F a] (F a *! F b))
-> Free '[F a] (F b ~~> (F a *! F b))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: [Syntax k]). Cast x '[F b, F a] => Free x (F b)
y -> Free '[F b, F a] (F a)
forall (x :: [Syntax k]). Cast x '[F a] => Free x (F a)
x Free '[F b, F a] (F a)
-> Free '[F b, F a] (F b) -> Free '[F b, F a] (F a && F b)
forall k (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i a -> Free i b -> Free i (a && b)
:& Free '[F b, F a] (F b)
forall (x :: [Syntax k]). Cast x '[F b, F a] => Free x (F b)
y)))

-- | Flip the argument order of a 3-argument curried function, applying the last argument
-- twice. This exercises three levels of nested 'lam' and 'Cast' weakening across all of them.
--
-- >>> import Prelude (Bool (..))
-- >>> flipCurried3 @Bool @Bool @Bool (\_ a _ -> a) True False
-- True
flipCurried3
  :: forall {k} a b c. (BiCCC k, Ob (a :: k), Ob b, Ob c) => (b ~~> a ~~> b ~~> c) ~> (a ~~> b ~~> c)
flipCurried3 :: forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(b ~~> (a ~~> (b ~~> c))) ~> (a ~~> (b ~~> c))
flipCurried3 =
  forall {k} (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
forall (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
toCCC @(F b ~~> (F a ~~> (F b ~~> F c))) @(F a ~~> (F b ~~> F c))
    (((forall (x :: [Syntax k]).
  Cast x '[F b --> (F a --> (F b --> F c))] =>
  Free x (F b --> (F a --> (F b --> F c))))
 -> Free '[F b --> (F a --> (F b --> F c))] (F a --> (F b --> F c)))
-> Free
     '[] ((F b --> (F a --> (F b --> F c))) ~~> (F a --> (F b --> F c)))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: [Syntax k]).
Cast x '[F b --> (F a --> (F b --> F c))] =>
Free x (F b --> (F a --> (F b --> F c)))
x -> ((forall (x :: [Syntax k]).
  Cast x '[F a, F b --> (F a --> (F b --> F c))] =>
  Free x (F a))
 -> Free '[F a, F b --> (F a --> (F b --> F c))] (F b --> F c))
-> Free '[F b --> (F a --> (F b --> F c))] (F a ~~> (F b --> F c))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: [Syntax k]).
Cast x '[F a, F b --> (F a --> (F b --> F c))] =>
Free x (F a)
y -> ((forall (x :: [Syntax k]).
  Cast x '[F b, F a, F b --> (F a --> (F b --> F c))] =>
  Free x (F b))
 -> Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F c))
-> Free '[F a, F b --> (F a --> (F b --> F c))] (F b ~~> F c)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: [Syntax k]).
Cast x '[F b, F a, F b --> (F a --> (F b --> F c))] =>
Free x (F b)
z -> ((Free
  '[F b, F a, F b --> (F a --> (F b --> F c))]
  (F b --> (F a --> (F b --> F c)))
Free
  '[F b, F a, F b --> (F a --> (F b --> F c))]
  (F b ~~> (F a --> (F b --> F c)))
forall (x :: [Syntax k]).
Cast x '[F b --> (F a --> (F b --> F c))] =>
Free x (F b --> (F a --> (F b --> F c)))
x Free
  '[F b, F a, F b --> (F a --> (F b --> F c))]
  (F b ~~> (F a --> (F b --> F c)))
-> Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F b)
-> Free
     '[F b, F a, F b --> (F a --> (F b --> F c))]
     (F a --> (F b --> F c))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i (a ~~> b) -> Free i a -> Free i b
$ Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F b)
forall (x :: [Syntax k]).
Cast x '[F b, F a, F b --> (F a --> (F b --> F c))] =>
Free x (F b)
z) Free
  '[F b, F a, F b --> (F a --> (F b --> F c))]
  (F a ~~> (F b --> F c))
-> Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F a)
-> Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F b --> F c)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i (a ~~> b) -> Free i a -> Free i b
$ Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F a)
forall (x :: [Syntax k]).
Cast x '[F a, F b --> (F a --> (F b --> F c))] =>
Free x (F a)
y) Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F b ~~> F c)
-> Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F b)
-> Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F c)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i (a ~~> b) -> Free i a -> Free i b
$ Free '[F b, F a, F b --> (F a --> (F b --> F c))] (F b)
forall (x :: [Syntax k]).
Cast x '[F b, F a, F b --> (F a --> (F b --> F c))] =>
Free x (F b)
z))))

-- | Swap a sum, via 'either'.
--
-- >>> import Prelude (Bool (..), Either (..))
-- >>> swapSum @Bool @Bool (Left True)
-- Right True
-- >>> swapSum @Bool @Bool (Right False)
-- Left False
swapSum :: forall {k} a b. (BiCCC k, Ob (a :: k), Ob b) => (a || b) ~> (b || a)
swapSum :: forall {k} (a :: k) (b :: k).
(BiCCC k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapSum = forall {k} (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
forall (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
toCCC @(F a || F b) @(F b || F a) (((forall (x :: Ctx k). Cast x '[F a + F b] => Free x (F a + F b))
 -> Free '[F a + F b] (F b + F a))
-> Free '[] ((F a + F b) ~~> (F b + F a))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: Ctx k). Cast x '[F a + F b] => Free x (F a + F b)
x -> Free '[F a + F b] (F a ~~> (F b + F a))
-> Free '[F a + F b] (F b ~~> (F b + F a))
-> Free '[F a + F b] (F a || F b)
-> Free '[F a + F b] (F b + F a)
forall {k} (a :: Syntax k) (b :: Syntax k) (c :: Syntax k)
       (i :: Ctx k).
(KnownCtx i, Ob a, Ob b, Ob c) =>
Free i (a ~~> c) -> Free i (b ~~> c) -> Free i (a || b) -> Free i c
either (((forall (x :: Ctx k). Cast x '[F a, F a + F b] => Free x (F a))
 -> Free '[F a, F a + F b] (F b + F a))
-> Free '[F a + F b] (F a ~~> (F b + F a))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: Ctx k). Cast x '[F a, F a + F b] => Free x (F a)
y -> Free '[F a, F a + F b] (F a) -> Free '[F a, F a + F b] (F b || F a)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i b -> Free i (a || b)
rgt Free '[F a, F a + F b] (F a)
forall (x :: Ctx k). Cast x '[F a, F a + F b] => Free x (F a)
y)) (((forall (x :: Ctx k). Cast x '[F b, F a + F b] => Free x (F b))
 -> Free '[F b, F a + F b] (F b + F a))
-> Free '[F a + F b] (F b ~~> (F b + F a))
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: Ctx k). Cast x '[F b, F a + F b] => Free x (F b)
y -> Free '[F b, F a + F b] (F b) -> Free '[F b, F a + F b] (F b || F a)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(Ob a, Ob b) =>
Free i a -> Free i (a || b)
lft Free '[F b, F a + F b] (F b)
forall (x :: Ctx k). Cast x '[F b, F a + F b] => Free x (F b)
y)) Free '[F a + F b] (F a + F b)
Free '[F a + F b] (F a || F b)
forall (x :: Ctx k). Cast x '[F a + F b] => Free x (F a + F b)
x))

-- | Eliminate a sum by applying whichever of the two functions matches the branch actually
-- present.
--
-- >>> import Prelude (Bool (..), Either (..), not)
-- >>> caseEither @Bool @Bool @Bool (Left True, (not, id))
-- False
-- >>> caseEither @Bool @Bool @Bool (Right True, (not, id))
-- True
caseEither
  :: forall {k} (a :: k) b c. (BiCCC k, Ob a, Ob b, Ob c) => ((a || b) && ((a ~~> c) && (b ~~> c))) ~> c
caseEither :: forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && ((a ~~> c) && (b ~~> c))) ~> c
caseEither =
  forall {k} (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
forall (a :: Syntax k) (b :: Syntax k).
(BiCCC k, Ob a, Ob b) =>
Free '[] (a ~~> b) -> Lower Id a ~> Lower Id b
toCCC @((F a || F b) && ((F a ~~> F c) && (F b ~~> F c))) @(F c)
    (((forall (x :: Ctx k).
  Cast x '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] =>
  Free x ((F a + F b) *! ((F a --> F c) *! (F b --> F c))))
 -> Free '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F c))
-> Free
     '[] (((F a + F b) *! ((F a --> F c) *! (F b --> F c))) ~~> F c)
forall {k} (a :: Syntax k) (b :: Syntax k) (i :: Ctx k).
(KnownCtx i, Ob a, Ob b) =>
((forall (x :: Ctx k). Cast x (a : i) => Free x a)
 -> Free (a : i) b)
-> Free i (a ~~> b)
lam (\forall (x :: Ctx k).
Cast x '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] =>
Free x ((F a + F b) *! ((F a --> F c) *! (F b --> F c)))
p -> let (Free '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F a + F b)
ab :& Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))]
  ((F a --> F c) *! (F b --> F c))
q) = Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))]
  ((F a + F b) *! ((F a --> F c) *! (F b --> F c)))
forall (x :: Ctx k).
Cast x '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] =>
Free x ((F a + F b) *! ((F a --> F c) *! (F b --> F c)))
p in let (Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F a --> F c)
ac :& Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F b --> F c)
bc) = Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))]
  ((F a --> F c) *! (F b --> F c))
q in Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F a ~~> F c)
-> Free
     '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F b ~~> F c)
-> Free
     '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F a || F b)
-> Free '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F c)
forall {k} (a :: Syntax k) (b :: Syntax k) (c :: Syntax k)
       (i :: Ctx k).
(KnownCtx i, Ob a, Ob b, Ob c) =>
Free i (a ~~> c) -> Free i (b ~~> c) -> Free i (a || b) -> Free i c
either Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F a --> F c)
Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F a ~~> F c)
ac Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F b --> F c)
Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F b ~~> F c)
bc Free '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F a + F b)
Free
  '[(F a + F b) *! ((F a --> F c) *! (F b --> F c))] (F a || F b)
ab))