{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE RecursiveDo #-}

-- | A small HOAS front end for building morphisms in any symmetric monoidal category, the linear
-- counterpart of "Proarrow.Tools.CCC". Each variable is used exactly once: the functions on terms
-- are linear, so GHC's linear types check that every variable is used once, and a 'Term' is
-- indexed by its context, which is exactly the variables it uses. So a variable is the identity
-- on its own type, and no copying or discarding is ever generated. Terms with disjoint contexts
-- combine by merging the contexts, which only reorders wires. Functions on terms need
-- @LinearTypes@ and linear arrows, e.g. @'Term' d g a %1 -> 'Term' d g b@.
--
-- Types are 'SYN' expressions, interpreted in the target category by 'Interp'. Their tensor is a
-- constructor, so 'split' can take a term's type apart, which the target's own @**@, a type
-- family, would not allow.
--
-- Every variable has an id, the number of binders around it, and a context lists its variables
-- by descending id. Merging compares ids, so it only reduces where the depths are known, which is
-- the case for terms built directly inside 'toSMC'. A reusable piece that binds variables of its
-- own is compiled on its own and used through 'call'.
--
-- The module also provides @do@ notation, for use with @QualifiedDo@:
--
-- > import Prelude hiding ((*))
-- > import Proarrow.Tools.SMC (SYN (..), lift, toSMC, (*))
-- > import Proarrow.Tools.SMC qualified as SMC
-- >
-- > rot2T = toSMC @(F a :** F b :** F c) \x -> SMC.do
-- >   (b, c, a) <- lift @(F a :** F b :** F c) @(F b :** F c :** F a) rotT x
-- >   c * a * b
--
-- Without the import of '(*)', Prelude's is used on terms, and GHC reports that as variables used
-- more than once (@Many@ against @One@) and mismatched depths, not as a missing instance.
--
-- A bind takes its right hand side apart with a pattern of (nested) tuples, as 'split' does, and
-- the rest of the block must use every variable exactly once. The argument of 'toSMC' is such a
-- pattern too, as in 'rotT', and @()@ there compiles a term without inputs.
--
-- With @RecursiveDo@, a @rec@ block traces, so it needs a traced monoidal category. Its variables
-- that are used before they are bound are fed back, and the others are passed on to the rest of
-- the block. GHC's translation of @rec@ passes every variable of the block to its end again,
-- including the ones a later statement of the block already used, so only such blocks work
-- where no statement uses a variable bound by an earlier one. A block of a single statement always
-- qualifies, and a nested pattern lets one statement bind everything:
--
-- > rec ((am, bp), (bm, cp)) <- lift g (ap * bm) * lift f (bp * cm)
--
-- 'loop' traces without GHC's translation, so it has neither restriction, but the type of the fed
-- back variable has to be given.
--
-- The module is inspired by Bernardy and Spiwack,
-- [Evaluating Linear Functions to Symmetric Monoidal Categories](https://arxiv.org/abs/2103.06195), whose
-- @P k r a@ ports correspond to 'Term', @encode@ to 'lift', @decode@ to 'toSMC', @(!:)@ to
-- '(*)' and @split@ to 'split'. Unlike their implementation, it keeps the context thinned instead
-- of computing in the cartesian structure and arguing afterwards that the result is monoidal.
module Proarrow.Tools.SMC
  ( -- * Types
    SYN (..)
  , Interp
  , KnownObj (..)
  , synOb

    -- * Terms
  , Term (..)
  , toSMC
  , lift
  , dup
  , drop
  , call
  , (*)
  , split
  , unit
  , lam
  , loop
  , produce
  , annihilate
  , (!)

    -- * Inputs and outputs
    -- $inout
  , Consumer
  , Command
  , type (:##)
  , cut
  , (|>)
  , accept
  , emit
  , par
  , both

    -- * Additives
    -- $additives
  , with
  , exl
  , exr
  , absorb
  , inl
  , inr
  , caseOf
  , absurd

    -- * Contexts
  , Ctx
  , Mul
  , KnownCtx
  , ctxOb
  , withCtxOb
  , Union
  , Merge (..)
  , snoc
  , snoc2
  , push2

    -- * Do notation
  , (>>=)
  , return
  , mfix
  , fail
  , Bind
  , Binds
  , Pat
  , Ret
  , Rec
  , RecVars

    -- * Examples
  , swapT
  , applyT
  , curryT
  , rotT
  , traceT
  , loopT
  , loopCC
  , snakeT
  , snakeDualT
  , combineDualT
  , dniT
  , dneT
  , contraT
  , parSwapT
  , weakDistT
  , distT
  , swapEitherT
  , bothWaysT
  ) where

import Data.Kind (Constraint, Type)
import GHC.Exts (Multiplicity (..))
import GHC.TypeLits (ErrorMessage (..), TypeError)
import GHC.TypeNats (CmpNat, Nat, type (+))
import Prelude (Ordering (..), type (~))
import Prelude qualified as P

import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , Tensor
  , associator'
  , associatorInv'
  )
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CompactClosed (CompactClosed (..))
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Category.Monoidal.IsoMix (IsoMix (..))
import Proarrow.Category.Monoidal.StarAutonomous (Par, StarAutonomous (..), dualityCounitSA)
import Proarrow.Category.Monoidal.Strength (Costrong (..), TracedMonoidal, trace)
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CategoryOf (..), Promonad (..), obj)
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (Comonoid (..))
import Proarrow.Object (Obj)

infixl 7 *
infixl 1 |>
infixl 8 !
infixl 7 :**
infixl 7 :##
infixl 6 :&&
infixl 6 :||
infixr 5 :->

-- | Type expressions over the objects of @k@: an object of @k@, the unit, the tensor, the
-- internal hom and the dual, and the additives: the product and its unit 'Top', and the
-- coproduct and its unit 'Zero'.
type data SYN k
  = F k
  | I
  | SYN k :** SYN k
  | SYN k :-> SYN k
  | D (SYN k)
  | SYN k :&& SYN k
  | Top
  | SYN k :|| SYN k
  | Zero

-- | The object of @k@ a type expression stands for.
type Interp :: forall {k}. SYN k -> k
type family Interp s where
  Interp (F a) = a
  Interp I = Unit
  Interp (a :** b) = Interp a ** Interp b
  Interp (a :-> b) = Interp a ~~> Interp b
  Interp (D a) = Dual (Interp a)
  Interp (a :&& b) = Interp a && Interp b
  Interp Top = TerminalObject
  Interp (a :|| b) = Interp a || Interp b
  Interp Zero = InitialObject

-- | Type expressions whose 'Interp' is an object, given that their leaves are.
type KnownObj :: forall {k}. SYN k -> Constraint
class (CategoryOf k) => KnownObj (s :: SYN k) where
  withSynOb :: ((Ob (Interp s)) => r) -> r

instance (CategoryOf k, Ob (a :: k)) => KnownObj (F a) where
  withSynOb :: forall r. (Ob (Interp (F a)) => r) -> r
withSynOb Ob (Interp (F a)) => r
r = r
Ob (Interp (F a)) => r
r

instance (Monoidal k) => KnownObj (I :: SYN k) where
  withSynOb :: forall r. (Ob (Interp I) => r) -> r
withSynOb Ob (Interp I) => r
r = r
Ob (Interp I) => r
r

instance (Monoidal k, KnownObj a, KnownObj (b :: SYN k)) => KnownObj (a :** b) where
  withSynOb :: forall r. (Ob (Interp (a :** b)) => r) -> r
withSynOb Ob (Interp (a :** b)) => r
r = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @(Interp a) @(Interp b) r
Ob (Interp a ** Interp b) => r
Ob (Interp (a :** b)) => r
r))

instance (Closed k, KnownObj a, KnownObj (b :: SYN k)) => KnownObj (a :-> b) where
  withSynOb :: forall r. (Ob (Interp (a :-> b)) => r) -> r
withSynOb Ob (Interp (a :-> b)) => r
r = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b (forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(Interp a) @(Interp b) r
Ob (Interp a ~~> Interp b) => r
Ob (Interp (a :-> b)) => r
r))

instance (StarAutonomous k, KnownObj (a :: SYN k)) => KnownObj (D a) where
  withSynOb :: forall r. (Ob (Interp (D a)) => r) -> r
withSynOb Ob (Interp (D a)) => r
r = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @(Interp a) r
Ob (Dual (Interp a)) => r
Ob (Interp (D a)) => r
r)

instance (HasBinaryProducts k, KnownObj a, KnownObj (b :: SYN k)) => KnownObj (a :&& b) where
  withSynOb :: forall r. (Ob (Interp (a :&& b)) => r) -> r
withSynOb Ob (Interp (a :&& b)) => r
r = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b (forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @(Interp a) @(Interp b) r
Ob (Interp a && Interp b) => r
Ob (Interp (a :&& b)) => r
r))

instance (HasTerminalObject k) => KnownObj (Top :: SYN k) where
  withSynOb :: forall r. (Ob (Interp Top) => r) -> r
withSynOb Ob (Interp Top) => r
r = r
Ob (Interp Top) => r
r

instance (HasBinaryCoproducts k, KnownObj a, KnownObj (b :: SYN k)) => KnownObj (a :|| b) where
  withSynOb :: forall r. (Ob (Interp (a :|| b)) => r) -> r
withSynOb Ob (Interp (a :|| b)) => r
r = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b (forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @(Interp a) @(Interp b) r
Ob (Interp a || Interp b) => r
Ob (Interp (a :|| b)) => r
r))

instance (HasInitialObject k) => KnownObj (Zero :: SYN k) where
  withSynOb :: forall r. (Ob (Interp Zero) => r) -> r
withSynOb Ob (Interp Zero) => r
r = r
Ob (Interp Zero) => r
r

-- | The identity on the object a type expression stands for.
synOb :: forall {k} (s :: SYN k). (KnownObj s) => Obj (Interp s)
synOb :: forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
synOb = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @s (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Interp s))

-- | A context: the variables a term uses, each with its id and type, by descending id.
type Ctx :: Type -> Type
type Ctx k = [(Nat, SYN k)]

-- | The type standing in for a context: the tensor of its variables' types, with the most
-- recently bound variable on the right. A single variable is just its type, so a variable is the
-- identity. The cost is that @Mul ('(n, a) ': g)@ only reduces once @g@ is known to be empty or
-- not, which 'ctxCase' tells.
type Mul :: forall {k}. Ctx k -> SYN k
type family Mul g where
  Mul '[] = I
  Mul '[ '(n, a)] = a
  Mul ('(n, a) ': g) = Mul g :** a

-- | A term at binding depth @d@ with context @g@ and type @a@: a morphism from the tensor of
-- the context to @a@.
type Term :: forall {k}. Nat -> Ctx k -> SYN k -> Type
data Term d g a where
  MkTerm :: (Interp (Mul g) ~> Interp a) %Many -> Term d g a

-- | A context that is known to be empty or not, all the way down.
type KnownCtx :: forall {k}. Ctx k -> Constraint
class KnownCtx (g :: Ctx k) where
  -- | Case analysis on the context, which is what lets @'Mul' ('(n, a) ': g)@ reduce.
  ctxCase :: ((g ~ '[]) => r) -> (forall n a g'. (g ~ ('(n, a) ': g'), KnownObj a, KnownCtx g') => r) -> r

instance KnownCtx ('[] :: Ctx k) where
  ctxCase :: forall r.
(('[] ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    ('[] ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase ('[] ~ '[]) => r
e forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
('[] ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
r
_ = r
('[] ~ '[]) => r
e

instance (KnownObj a, KnownCtx g) => KnownCtx ('(n, a) ': g) where
  ctxCase :: forall r.
((('(n, a) : g) ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (('(n, a) : g) ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase (('(n, a) : g) ~ '[]) => r
_ forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
(('(n, a) : g) ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
r
c = r
forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
(('(n, a) : g) ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
r
c

-- | The tensor of a context is an object.
withCtxOb :: forall {k} (g :: Ctx k) r. (Monoidal k, KnownCtx g) => ((Ob (Interp (Mul g))) => r) -> r
withCtxOb :: forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb Ob (Interp (Mul g)) => r
r =
  forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g
    r
(g ~ '[]) => r
Ob (Interp (Mul g)) => r
r
    ( \ @_ @a @g' ->
        forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g' (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a r
Ob (Interp a) => r
Ob (Interp (Mul g)) => r
r) (forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g' (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @(Interp (Mul g')) @(Interp a) r
Ob (Interp (Mul g') ** Interp a) => r
Ob (Interp (Mul g)) => r
r)))
    )

-- | The identity on the tensor of a context.
ctxOb :: forall {k} (g :: Ctx k). (Monoidal k, KnownCtx g) => Obj (Interp (Mul g))
ctxOb :: forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb = forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Interp (Mul g)))

-- | A new variable on the right of a context: a unitor if the context was empty, and nothing
-- otherwise.
snoc
  :: forall {k} n (a :: SYN k) g
   . (Monoidal k, KnownObj a, KnownCtx g) => Interp (Mul g) ** Interp a ~> Interp (Mul ('(n, a) ': g))
snoc :: forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc = forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (Unit ** Interp a) ~> Interp a
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
Ob (Interp a) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(n, a) ': g))

-- | Two new variables on the right of a context, from their tensor: a unitor if the context was
-- empty, and an associator otherwise.
snoc2
  :: forall {k} n (a :: SYN k) m b g
   . (Monoidal k, KnownObj a, KnownObj b, KnownCtx g)
  => Interp (Mul g) ** (Interp a ** Interp b) ~> Interp (Mul ('(m, b) ': '(n, a) ': g))
snoc2 :: forall {k} (n :: Nat) (a :: SYN k) (m :: Nat) (b :: SYN k)
       (g :: Ctx k).
(Monoidal k, KnownObj a, KnownObj b, KnownCtx g) =>
(Interp (Mul g) ** (Interp a ** Interp b))
~> Interp (Mul ('(m, b) : '(n, a) : g))
snoc2 = forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @(a :** b) (Unit ** (Interp a ** Interp b)) ~> (Interp a ** Interp b)
(Interp (Mul g) ** (Interp a ** Interp b))
~> (Interp (Mul ('(n, a) : g)) ** Interp b)
Ob (Interp (a :** b)) =>
(Interp (Mul g) ** (Interp a ** Interp b))
~> (Interp (Mul ('(n, a) : g)) ** Interp b)
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor) (Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp a)
-> Obj (Interp b)
-> (Interp (Mul ('(n, a) : g')) ** (Interp a ** Interp b))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp a) ** Interp b)
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b))

-- | The context of two terms used side by side.
type Union :: forall {k}. Ctx k -> Ctx k -> Ctx k
type family Union g1 g2 where
  Union '[] g2 = g2
  Union g1 '[] = g1
  Union ('(n, a) ': g1) ('(m, b) ': g2) = UnionBy (CmpNat n m) ('(n, a) ': g1) ('(m, b) ': g2)

type UnionBy :: forall {k}. Ordering -> Ctx k -> Ctx k -> Ctx k
type family UnionBy o g1 g2 where
  UnionBy GT (x ': g1) g2 = x ': Union g1 g2
  UnionBy LT g1 (y ': g2) = y ': Union g1 g2
  UnionBy EQ _ _ = TypeError (Text "Proarrow.Tools.SMC: a variable is used more than once")

-- | Split the tensor of a merged context into the tensors of the two contexts it came from, and
-- back. This is where the wires are reordered, and the only place 'swap' is used.
type Merge :: forall {k}. Ctx k -> Ctx k -> Constraint
class (KnownCtx g1, KnownCtx g2) => Merge (g1 :: Ctx k) g2 where
  merge :: Interp (Mul (Union g1 g2)) ~> Interp (Mul g1) ** Interp (Mul g2)
  unmerge :: Interp (Mul g1) ** Interp (Mul g2) ~> Interp (Mul (Union g1 g2))

instance (Monoidal k, KnownCtx g2) => Merge ('[] :: Ctx k) g2 where
  merge :: Interp (Mul (Union '[] g2))
~> (Interp (Mul '[]) ** Interp (Mul g2))
merge = forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g2 Interp (Mul g2) ~> (Unit ** Interp (Mul g2))
Ob (Interp (Mul g2)) =>
Interp (Mul g2) ~> (Unit ** Interp (Mul g2))
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  unmerge :: (Interp (Mul '[]) ** Interp (Mul g2))
~> Interp (Mul (Union '[] g2))
unmerge = forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g2 (Unit ** Interp (Mul g2)) ~> Interp (Mul g2)
Ob (Interp (Mul g2)) =>
(Unit ** Interp (Mul g2)) ~> Interp (Mul g2)
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor

instance (Monoidal k, KnownCtx ('(n, a) ': g1)) => Merge ('(n, a) ': g1 :: Ctx k) '[] where
  merge :: Interp (Mul (Union ('(n, a) : g1) '[]))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul '[]))
merge = forall (g :: [(Nat, SYN k)]) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(n, a) ': g1) Interp (Mul ('(n, a) : g1))
~> (Interp (Mul ('(n, a) : g1)) ** Unit)
Ob (Interp (Mul ('(n, a) : g1))) =>
Interp (Mul ('(n, a) : g1))
~> (Interp (Mul ('(n, a) : g1)) ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  unmerge :: (Interp (Mul ('(n, a) : g1)) ** Interp (Mul '[]))
~> Interp (Mul (Union ('(n, a) : g1) '[]))
unmerge = forall (g :: [(Nat, SYN k)]) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(n, a) ': g1) (Interp (Mul ('(n, a) : g1)) ** Unit)
~> Interp (Mul ('(n, a) : g1))
Ob (Interp (Mul ('(n, a) : g1))) =>
(Interp (Mul ('(n, a) : g1)) ** Unit)
~> Interp (Mul ('(n, a) : g1))
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor

instance
  ( Monoidal k
  , KnownObj a
  , KnownObj b
  , KnownCtx g1
  , KnownCtx g2
  , MergeBy (CmpNat n m) ('(n, a) ': g1 :: Ctx k) ('(m, b) ': g2)
  )
  => Merge ('(n, a) ': g1 :: Ctx k) ('(m, b) ': g2)
  where
  merge :: Interp (Mul (Union ('(n, a) : g1) ('(m, b) : g2)))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
merge = forall (o :: Ordering) (g1 :: Ctx k) (g2 :: Ctx k).
MergeBy o g1 g2 =>
Interp (Mul (UnionBy o g1 g2))
~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (o :: Ordering) (g1 :: Ctx k) (g2 :: Ctx k).
MergeBy o g1 g2 =>
Interp (Mul (UnionBy o g1 g2))
~> (Interp (Mul g1) ** Interp (Mul g2))
mergeBy @(CmpNat n m) @('(n, a) ': g1) @('(m, b) ': g2)
  unmerge :: (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
~> Interp (Mul (Union ('(n, a) : g1) ('(m, b) : g2)))
unmerge = forall (o :: Ordering) (g1 :: Ctx k) (g2 :: Ctx k).
MergeBy o g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2))
~> Interp (Mul (UnionBy o g1 g2))
forall {k} (o :: Ordering) (g1 :: Ctx k) (g2 :: Ctx k).
MergeBy o g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2))
~> Interp (Mul (UnionBy o g1 g2))
unmergeBy @(CmpNat n m) @('(n, a) ': g1) @('(m, b) ': g2)

-- | 'merge' and 'unmerge' for two non-empty contexts, by which of the two has the larger head id.
type MergeBy :: forall {k}. Ordering -> Ctx k -> Ctx k -> Constraint
class (KnownCtx g1, KnownCtx g2) => MergeBy o (g1 :: Ctx k) g2 where
  mergeBy :: Interp (Mul (UnionBy o g1 g2)) ~> Interp (Mul g1) ** Interp (Mul g2)
  unmergeBy :: Interp (Mul g1) ** Interp (Mul g2) ~> Interp (Mul (UnionBy o g1 g2))

-- The union of two non-empty contexts is not empty, so its tensor splits off the newest variable
-- as is, which the equality says for GHC. If the newest variable is alone on its side, merging is
-- one swap or nothing.
instance
  ( SymMonoidal k
  , Merge g1 ('(m, b) ': g2)
  , KnownObj (a :: SYN k)
  , KnownObj b
  , Mul ('(n, a) ': Union g1 ('(m, b) ': g2)) ~ (Mul (Union g1 ('(m, b) ': g2)) :** a)
  )
  => MergeBy GT ('(n, a) ': g1) ('(m, b) ': g2)
  where
  mergeBy :: Interp (Mul (UnionBy 'GT ('(n, a) : g1) ('(m, b) : g2)))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
mergeBy =
    forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(m, b) ': g2)
      ( forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a
          ( forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g1
              (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Interp (Mul ('(m, b) ': g2))) @(Interp a))
              ( Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp a)
-> Obj (Interp (Mul ('(m, b) : g2)))
-> (Interp (Mul ('(n, a) : g'))
    ** (Interp a ** Interp (Mul ('(m, b) : g2))))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp a)
       ** Interp (Mul ('(m, b) : g2)))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': g2))
                  ((Interp (Mul ('(n, a) : g'))
  ** (Interp a ** Interp (Mul ('(m, b) : g2))))
 ~> ((Interp (Mul ('(n, a) : g')) ** Interp a)
     ** Interp (Mul ('(m, b) : g2))))
-> ((Interp
       (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
     ** Interp a)
    ~> (Interp (Mul ('(n, a) : g'))
        ** (Interp a ** Interp (Mul ('(m, b) : g2)))))
-> (Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
    ** Interp a)
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp a)
       ** Interp (Mul ('(m, b) : g2)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1 Obj (Interp (Mul ('(n, a) : g')))
-> ((Interp (Mul ('(m, b) : g2)) ** Interp a)
    ~> (Interp a ** Interp (Mul ('(m, b) : g2))))
-> (Interp (Mul ('(n, a) : g'))
    ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp a ** Interp (Mul ('(m, b) : g2))))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Interp (Mul ('(m, b) ': g2))) @(Interp a))
                  ((Interp (Mul ('(n, a) : g'))
  ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
 ~> (Interp (Mul ('(n, a) : g'))
     ** (Interp a ** Interp (Mul ('(m, b) : g2)))))
-> ((Interp
       (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
     ** Interp a)
    ~> (Interp (Mul ('(n, a) : g'))
        ** (Interp (Mul ('(m, b) : g2)) ** Interp a)))
-> (Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
    ** Interp a)
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp a ** Interp (Mul ('(m, b) : g2))))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp (Mul ('(m, b) : g2)))
-> Obj (Interp a)
-> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
    ** Interp a)
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': g2)) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a)
                  (((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
  ** Interp a)
 ~> (Interp (Mul ('(n, a) : g'))
     ** (Interp (Mul ('(m, b) : g2)) ** Interp a)))
-> ((Interp
       (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
     ** Interp a)
    ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
        ** Interp a))
-> (Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
    ** Interp a)
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @g1 @('(m, b) ': g2) (Interp (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
 ~> (Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2))))
-> Obj (Interp a)
-> (Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
    ** Interp a)
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
       ** Interp a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a)
              )
          )
      )
  unmergeBy :: (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
~> Interp (Mul (UnionBy 'GT ('(n, a) : g1) ('(m, b) : g2)))
unmergeBy =
    forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(m, b) ': g2)
      ( forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a
          ( forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g1
              (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Interp a) @(Interp (Mul ('(m, b) ': g2))))
              ( (forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
unmerge @g1 @('(m, b) ': g2) ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
 ~> Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2))))
-> Obj (Interp a)
-> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
    ** Interp a)
   ~> (Interp
         (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
       ** Interp a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a)
                  (((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
  ** Interp a)
 ~> (Interp
       (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
     ** Interp a))
-> (((Interp (Mul ('(n, a) : g')) ** Interp a)
     ** Interp (Mul ('(m, b) : g2)))
    ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
        ** Interp a))
-> ((Interp (Mul ('(n, a) : g')) ** Interp a)
    ** Interp (Mul ('(m, b) : g2)))
   ~> (Interp
         (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
       ** Interp a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp (Mul ('(m, b) : g2)))
-> Obj (Interp a)
-> (Interp (Mul ('(n, a) : g'))
    ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
       ** Interp a)
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': g2)) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a)
                  ((Interp (Mul ('(n, a) : g'))
  ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
 ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
     ** Interp a))
-> (((Interp (Mul ('(n, a) : g')) ** Interp a)
     ** Interp (Mul ('(m, b) : g2)))
    ~> (Interp (Mul ('(n, a) : g'))
        ** (Interp (Mul ('(m, b) : g2)) ** Interp a)))
-> ((Interp (Mul ('(n, a) : g')) ** Interp a)
    ** Interp (Mul ('(m, b) : g2)))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
       ** Interp a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1 Obj (Interp (Mul ('(n, a) : g')))
-> ((Interp a ** Interp (Mul ('(m, b) : g2)))
    ~> (Interp (Mul ('(m, b) : g2)) ** Interp a))
-> (Interp (Mul ('(n, a) : g'))
    ** (Interp a ** Interp (Mul ('(m, b) : g2))))
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Interp a) @(Interp (Mul ('(m, b) ': g2))))
                  ((Interp (Mul ('(n, a) : g'))
  ** (Interp a ** Interp (Mul ('(m, b) : g2))))
 ~> (Interp (Mul ('(n, a) : g'))
     ** (Interp (Mul ('(m, b) : g2)) ** Interp a)))
-> (((Interp (Mul ('(n, a) : g')) ** Interp a)
     ** Interp (Mul ('(m, b) : g2)))
    ~> (Interp (Mul ('(n, a) : g'))
        ** (Interp a ** Interp (Mul ('(m, b) : g2)))))
-> ((Interp (Mul ('(n, a) : g')) ** Interp a)
    ** Interp (Mul ('(m, b) : g2)))
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp a)
-> Obj (Interp (Mul ('(m, b) : g2)))
-> ((Interp (Mul ('(n, a) : g')) ** Interp a)
    ** Interp (Mul ('(m, b) : g2)))
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp a ** Interp (Mul ('(m, b) : g2))))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': g2))
              )
          )
      )

instance
  ( Monoidal k
  , Merge ('(n, a) ': g1) g2
  , KnownObj a
  , KnownObj (b :: SYN k)
  , Mul ('(m, b) ': Union ('(n, a) ': g1) g2) ~ (Mul (Union ('(n, a) ': g1) g2) :** b)
  )
  => MergeBy LT ('(n, a) ': g1) ('(m, b) ': g2)
  where
  mergeBy :: Interp (Mul (UnionBy 'LT ('(n, a) : g1) ('(m, b) : g2)))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
mergeBy =
    forall (g :: [(Nat, SYN k)]) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: [(Nat, SYN k)]).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g2
      (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': '(n, a) ': g1))
      ( Obj (Interp (Mul ('(n, a) : g1)))
-> Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp b)
-> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
    ** Interp b)
   ~> (Interp (Mul ('(n, a) : g1))
       ** (Interp (Mul ('(n, a) : g')) ** Interp b))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(n, a) ': g1)) (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g2) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
          (((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
  ** Interp b)
 ~> (Interp (Mul ('(n, a) : g1))
     ** (Interp (Mul ('(n, a) : g')) ** Interp b)))
-> ((Interp
       (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
     ** Interp b)
    ~> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
        ** Interp b))
-> (Interp
      (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
    ** Interp b)
   ~> (Interp (Mul ('(n, a) : g1))
       ** (Interp (Mul ('(n, a) : g')) ** Interp b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g1 :: [(Nat, SYN k)]) (g2 :: [(Nat, SYN k)]).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @('(n, a) ': g1) @g2 (Interp (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
 ~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g'))))
-> Obj (Interp b)
-> (Interp
      (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
    ** Interp b)
   ~> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
       ** Interp b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
      )
  unmergeBy :: (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
~> Interp (Mul (UnionBy 'LT ('(n, a) : g1) ('(m, b) : g2)))
unmergeBy =
    forall (g :: [(Nat, SYN k)]) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: [(Nat, SYN k)]).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g2
      (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': '(n, a) ': g1))
      ( (forall (g1 :: [(Nat, SYN k)]) (g2 :: [(Nat, SYN k)]).
Merge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
unmerge @('(n, a) ': g1) @g2 ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
 ~> Interp
      (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g'))))
-> Obj (Interp b)
-> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
    ** Interp b)
   ~> (Interp
         (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
       ** Interp b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
          (((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
  ** Interp b)
 ~> (Interp
       (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
     ** Interp b))
-> ((Interp (Mul ('(n, a) : g1))
     ** (Interp (Mul ('(n, a) : g')) ** Interp b))
    ~> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
        ** Interp b))
-> (Interp (Mul ('(n, a) : g1))
    ** (Interp (Mul ('(n, a) : g')) ** Interp b))
   ~> (Interp
         (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
       ** Interp b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Interp (Mul ('(n, a) : g1)))
-> Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp b)
-> (Interp (Mul ('(n, a) : g1))
    ** (Interp (Mul ('(n, a) : g')) ** Interp b))
   ~> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
       ** Interp b)
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(n, a) ': g1)) (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g2) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
      )

-- | The variable with id @n@: the identity on its type.
var :: forall {k} n (a :: SYN k) d. (CategoryOf k, KnownObj a) => Term d '[ '(n, a)] a
var :: forall {k} (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
var = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a ((Interp (Mul '[ '(n, a)]) ~> Interp a) -> Term d '[ '(n, a)] a
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Interp a)))

-- | Compile a function on terms to a morphism. Its argument is a pattern, as on the left of a bind
-- in @do@ notation: a variable, which must be used exactly once, @()@ for the unit, or a pair of
-- patterns.
toSMC
  :: forall {k} (a :: SYN k) b t cont
   . (Monoidal k, Binds t 0 a cont '[] b)
  => (t %1 -> cont)
  -> Interp a ~> Interp b
toSMC :: forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC t %1 -> cont
k = case forall (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
bound @0 @'[] @a @b t %1 -> cont
k of MkTerm Interp (Mul '[ '(0, a)]) ~> Interp b
f -> Interp a ~> Interp b
Interp (Mul '[ '(0, a)]) ~> Interp b
f

-- | Copy a term whose type is a comonoid, in "Proarrow.Tools.SMC": @(x1, x2) <- dup x@.
dup :: forall {k} (s :: SYN k) d g. (Comonoid (Interp s)) => Term d g s %1 -> Term d g (s :** s)
dup :: forall {k} (s :: SYN k) (d :: Nat) (g :: Ctx k).
Comonoid (Interp s) =>
Term d g s %1 -> Term d g (s :** s)
dup = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @s @(s :** s) Interp s ~> (Interp s ** Interp s)
Interp s ~> Interp (s :** s)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

-- | Discard a term whose type is a comonoid, in "Proarrow.Tools.SMC": @() <- drop x@.
drop :: forall {k} (s :: SYN k) d g. (Comonoid (Interp s)) => Term d g s %1 -> Term d g I
drop :: forall {k} (s :: SYN k) (d :: Nat) (g :: Ctx k).
Comonoid (Interp s) =>
Term d g s %1 -> Term d g I
drop = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @s @I Interp s ~> Unit
Interp s ~> Interp I
forall {k} (c :: k). Comonoid c => c ~> Unit
counit

-- | Lift a morphism of the target category to a function on terms.
lift :: forall {k} (a :: SYN k) b d g. (CategoryOf k) => (Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift :: forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift Interp a ~> Interp b
f (MkTerm Interp (Mul g) ~> Interp a
t) = (Interp (Mul g) ~> Interp b) -> Term d g b
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (Interp a ~> Interp b
f (Interp a ~> Interp b)
-> (Interp (Mul g) ~> Interp a) -> Interp (Mul g) ~> Interp b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Interp (Mul g) ~> Interp a
t)

-- | Use a function on terms inside another term, compiled on its own with 'toSMC', so that its
-- argument is a pattern too. This is how a reusable piece that binds variables of its own is used,
-- and unlike 'lift' of the compiled morphism it needs no type annotations.
call
  :: forall {k} (a :: SYN k) b d g t cont
   . (Monoidal k, Binds t 0 a cont '[] b)
  => (t %1 -> cont)
  -> Term d g a
  %1 -> Term d g b
call :: forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k) t
       cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Term d g a %1 -> Term d g b
call t %1 -> cont
f = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @a @b (forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @a @b t %1 -> cont
f)

-- | Two terms side by side. Their contexts must be disjoint.
(*)
  :: forall {k} d g1 g2 (a :: SYN k) b
   . (Monoidal k, Merge g1 g2)
  => Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
MkTerm Interp (Mul g1) ~> Interp a
f * :: forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* MkTerm Interp (Mul g2) ~> Interp b
g = (Interp (Mul (Union g1 g2)) ~> Interp (a :** b))
-> Term d (Union g1 g2) (a :** b)
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm ((Interp (Mul g1) ~> Interp a
f (Interp (Mul g1) ~> Interp a)
-> (Interp (Mul g2) ~> Interp b)
-> (Interp (Mul g1) ** Interp (Mul g2)) ~> (Interp a ** Interp b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Interp (Mul g2) ~> Interp b
g) ((Interp (Mul g1) ** Interp (Mul g2)) ~> (Interp a ** Interp b))
-> (Interp (Mul (Union g1 g2))
    ~> (Interp (Mul g1) ** Interp (Mul g2)))
-> Interp (Mul (Union g1 g2)) ~> (Interp a ** Interp b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @g1 @g2)

-- | Two new variables @(n, a)@ and @(m, b)@ on the right of the context @r@, for 'split'. When @r@
-- is empty the pair is the whole context.
push2
  :: forall {k} r n (a :: SYN k) m b g
   . (Monoidal k, KnownObj a, KnownObj b, Merge r g)
  => (Interp (Mul g) ~> Interp a ** Interp b)
  -> Interp (Mul (Union r g)) ~> Interp (Mul ('(m, b) ': '(n, a) ': r))
push2 :: forall {k} (r :: Ctx k) (n :: Nat) (a :: SYN k) (m :: Nat)
       (b :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownObj b, Merge r g) =>
(Interp (Mul g) ~> (Interp a ** Interp b))
-> Interp (Mul (Union r g)) ~> Interp (Mul ('(m, b) : '(n, a) : r))
push2 Interp (Mul g) ~> (Interp a ** Interp b)
p =
  forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @r
    Interp (Mul g) ~> (Interp a ** Interp b)
Interp (Mul (Union r g))
~> (Interp (Mul ('(n, a) : r)) ** Interp b)
(r ~ '[]) =>
Interp (Mul (Union r g))
~> (Interp (Mul ('(n, a) : r)) ** Interp b)
p
    (Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp a)
-> Obj (Interp b)
-> (Interp (Mul ('(n, a) : g')) ** (Interp a ** Interp b))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp a) ** Interp b)
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @r) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b) ((Interp (Mul ('(n, a) : g')) ** (Interp a ** Interp b))
 ~> ((Interp (Mul ('(n, a) : g')) ** Interp a) ** Interp b))
-> (Interp (Mul (Union ('(n, a) : g') g))
    ~> (Interp (Mul ('(n, a) : g')) ** (Interp a ** Interp b)))
-> Interp (Mul (Union ('(n, a) : g') g))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp a) ** Interp b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @r Obj (Interp (Mul ('(n, a) : g')))
-> (Interp (Mul g) ~> (Interp a ** Interp b))
-> (Interp (Mul ('(n, a) : g')) ** Interp (Mul g))
   ~> (Interp (Mul ('(n, a) : g')) ** (Interp a ** Interp b))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Interp (Mul g) ~> (Interp a ** Interp b)
p) ((Interp (Mul ('(n, a) : g')) ** Interp (Mul g))
 ~> (Interp (Mul ('(n, a) : g')) ** (Interp a ** Interp b)))
-> (Interp (Mul (Union ('(n, a) : g') g))
    ~> (Interp (Mul ('(n, a) : g')) ** Interp (Mul g)))
-> Interp (Mul (Union ('(n, a) : g') g))
   ~> (Interp (Mul ('(n, a) : g')) ** (Interp a ** Interp b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @r @g)

-- | Take a tensor apart: the continuation gets a variable for each side and must use both.
split
  :: forall {k} d g r (a :: SYN k) b c da db
   . (Monoidal k, KnownObj a, KnownObj b, Merge r g)
  => Term d g (a :** b)
  %1 -> ( Term da '[ '(d, a)] a
          %1 -> Term db '[ '(d + 1, b)] b
          %1 -> Term (d + 2) ('(d + 1, b) ': '(d, a) ': r) c
        )
  %1 -> Term d (Union r g) c
split :: forall {k} (d :: Nat) (g :: Ctx k) (r :: Ctx k) (a :: SYN k)
       (b :: SYN k) (c :: SYN k) (da :: Nat) (db :: Nat).
(Monoidal k, KnownObj a, KnownObj b, Merge r g) =>
Term d g (a :** b)
%1 -> (Term da '[ '(d, a)] a
       %1 -> Term db '[ '(d + 1, b)] b
       %1 -> Term (d + 2) ('(d + 1, b) : '(d, a) : r) c)
%1 -> Term d (Union r g) c
split (MkTerm Interp (Mul g) ~> Interp (a :** b)
p) Term da '[ '(d, a)] a
%1 -> Term db '[ '(d + 1, b)] b
%1 -> Term (d + 2) ('(d + 1, b) : '(d, a) : r) c
k = case Term da '[ '(d, a)] a
%1 -> Term db '[ '(d + 1, b)] b
%1 -> Term (d + 2) ('(d + 1, b) : '(d, a) : r) c
k (forall (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
forall {k} (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
var @d @a) (forall (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
forall {k} (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
var @(d + 1) @b) of
  MkTerm Interp (Mul ('(d + 1, b) : '(d, a) : r)) ~> Interp c
body -> (Interp (Mul (Union r g)) ~> Interp c) -> Term d (Union r g) c
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm ((Interp (Mul ('(d, a) : r)) ** Interp b) ~> Interp c
Interp (Mul ('(d + 1, b) : '(d, a) : r)) ~> Interp c
body ((Interp (Mul ('(d, a) : r)) ** Interp b) ~> Interp c)
-> (Interp (Mul (Union r g))
    ~> (Interp (Mul ('(d, a) : r)) ** Interp b))
-> Interp (Mul (Union r g)) ~> Interp c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (r :: Ctx k) (n :: Nat) (a :: SYN k) (m :: Nat) (b :: SYN k)
       (g :: Ctx k).
(Monoidal k, KnownObj a, KnownObj b, Merge r g) =>
(Interp (Mul g) ~> (Interp a ** Interp b))
-> Interp (Mul (Union r g)) ~> Interp (Mul ('(m, b) : '(n, a) : r))
forall {k} (r :: Ctx k) (n :: Nat) (a :: SYN k) (m :: Nat)
       (b :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownObj b, Merge r g) =>
(Interp (Mul g) ~> (Interp a ** Interp b))
-> Interp (Mul (Union r g)) ~> Interp (Mul ('(m, b) : '(n, a) : r))
push2 @r @d @a @(d + 1) @b @g Interp (Mul g) ~> (Interp a ** Interp b)
Interp (Mul g) ~> Interp (a :** b)
p)

-- | The unit, which uses no variables.
unit :: forall {k} d. (Monoidal k) => Term d ('[] :: Ctx k) I
unit :: forall {k} (d :: Nat). Monoidal k => Term d '[] I
unit = (Interp (Mul '[]) ~> Interp I) -> Term d '[] I
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm Unit ~> Unit
Interp (Mul '[]) ~> Interp I
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

-- | Bind a pattern, as for 'toSMC', whose variables the body must use exactly once. This needs the
-- category to be closed.
lam
  :: forall {k} d r (a :: SYN k) b t cont
   . (Closed k, Binds t d a cont r b)
  => (t %1 -> cont)
  %1 -> Term d r (a :-> b)
lam :: forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
(Closed k, Binds t d a cont r b) =>
(t %1 -> cont) %1 -> Term d r (a :-> b)
lam t %1 -> cont
k = case forall (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
bound @d @r @a @b t %1 -> cont
k of
  MkTerm Interp (Mul ('(d, a) : r)) ~> Interp b
body -> forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @r (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a ((Interp (Mul r) ~> Interp (a :-> b)) -> Term d r (a :-> b)
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @(Interp (Mul r)) @(Interp a) (Interp (Mul ('(d, a) : r)) ~> Interp b
body (Interp (Mul ('(d, a) : r)) ~> Interp b)
-> ((Interp (Mul r) ** Interp a) ~> Interp (Mul ('(d, a) : r)))
-> (Interp (Mul r) ** Interp a) ~> Interp b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc @d @a @r))))

-- | The body of a binder, with the pattern taking apart its new variable: what 'toSMC', 'lam',
-- 'loop' and 'accept' share.
bound
  :: forall {k} d r (a :: SYN k) b t cont
   . (Binds t d a cont r b)
  => (t %1 -> cont)
  %1 -> Term (d + 1) ('(d, a) ': r) b
bound :: forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
bound t %1 -> cont
k = forall (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
forall {k} (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
var @d @a @(d + 1) Term (d + 1) '[ '(d, a)] a
%1 -> (t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
forall k m t (p :: Multiplicity) cont r.
Bind k m t p cont r =>
m %1 -> (t %p -> cont) %1 -> r
>>= t %1 -> cont
k

-- | Trace: bind a pattern, as for 'toSMC', for the value fed back, whose variables the body must
-- use exactly once, and return it again next to the result. This needs the category to be traced.
loop
  :: forall {k} (u :: SYN k) b d r t cont
   . (TracedMonoidal k, KnownObj b, Binds t d u cont r (b :** u))
  => (t %1 -> cont)
  %1 -> Term d r b
loop :: forall {k} (u :: SYN k) (b :: SYN k) (d :: Nat) (r :: Ctx k) t
       cont.
(TracedMonoidal k, KnownObj b, Binds t d u cont r (b :** u)) =>
(t %1 -> cont) %1 -> Term d r b
loop t %1 -> cont
k = case forall (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
bound @d @r @u @(b :** u) t %1 -> cont
k of
  MkTerm Interp (Mul ('(d, u) : r)) ~> Interp (b :** u)
body ->
    forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @r
      (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @u (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b ((Interp (Mul r) ~> Interp b) -> Term d r b
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall {k} (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(Costrong Tensor p, Ob x, Ob y, Ob u, SymMonoidal k) =>
p (x ** u) (y ** u) -> p x y
forall (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(Costrong Tensor p, Ob x, Ob y, Ob u, SymMonoidal k) =>
p (x ** u) (y ** u) -> p x y
trace @(~>) @(Interp u) @(Interp (Mul r)) @(Interp b) (Interp (Mul ('(d, u) : r)) ~> (Interp b ** Interp u)
Interp (Mul ('(d, u) : r)) ~> Interp (b :** u)
body (Interp (Mul ('(d, u) : r)) ~> (Interp b ** Interp u))
-> ((Interp (Mul r) ** Interp u) ~> Interp (Mul ('(d, u) : r)))
-> (Interp (Mul r) ** Interp u) ~> (Interp b ** Interp u)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc @d @u @r)))))

-- | A new pair of wires, a variable and its dual, from nothing: the unit of the duality. This
-- needs the category to be compact closed.
produce :: forall {k} (a :: SYN k) d. (CompactClosed k, KnownObj a) => Term d '[] (a :** D a)
produce :: forall {k} (a :: SYN k) (d :: Nat).
(CompactClosed k, KnownObj a) =>
Term d '[] (a :** D a)
produce = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a ((Interp (Mul '[]) ~> Interp (a :** D a)) -> Term d '[] (a :** D a)
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall k (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
dualityUnit @k @(Interp a)))

-- | Join a dual and its wire into nothing: the counit of the duality, which an isomix category
-- has.
annihilate
  :: forall {k} (a :: SYN k) d g1 g2
   . (IsoMix k, KnownObj a, Merge g1 g2)
  => Consumer d g1 a %1 -> Term d g2 a %1 -> Term d (Union g1 g2) I
annihilate :: forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(IsoMix k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Term d (Union g1 g2) I
annihilate Consumer d g1 a
x Term d g2 a
y = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(D a :** a) @I (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall k (a :: k). (IsoMix k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @k @(Interp a))) (Consumer d g1 a
x Consumer d g1 a
%1 -> Term d g2 a %1 -> Term d (Union g1 g2) (D a :** a)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term d g2 a
y)

-- $inout
-- In a *-autonomous category a term of @'D' a@ consumes an @a@. Terms then read as in System L
-- (the μμ̃-calculus): a 'Term' produces, a 'Consumer' consumes, and a 'Command' is the two meeting
-- in a 'cut', a term of @'D' 'I'@. A command can have any number of inputs and outputs. None of
-- this needs compact closure: 'produce' does.

-- | A consumer of @a@: a term of its dual.
type Consumer :: forall {k}. Nat -> Ctx k -> SYN k -> Type
type Consumer d g a = Term d g (D a)

-- | A producer and a consumer meeting: a term of the unit of par.
type Command :: forall {k}. Nat -> Ctx k -> Type
type Command d g = Term d g (D I)

-- | Par, the dual of the tensor of the duals, interpreted as 'Proarrow.Category.Monoidal.StarAutonomous.Par'.
type (:##) :: forall {k}. SYN k -> SYN k -> SYN k
type a :## b = D (D a :** D b)

-- | A consumer meets a producer: @cut k t@ gives @t@ to @k@, like applying a continuation. This
-- needs the category to be *-autonomous.
cut
  :: forall {k} (a :: SYN k) d g1 g2
   . (StarAutonomous k, KnownObj a, Merge g1 g2)
  => Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
cut :: forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
cut Consumer d g1 a
x Term d g2 a
y = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(D a :** a) @(D I) (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall (a :: k).
(StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Dual Unit
forall {k} (a :: k).
(StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Dual Unit
dualityCounitSA @(Interp a))) (Consumer d g1 a
x Consumer d g1 a
%1 -> Term d g2 a %1 -> Term d (Union g1 g2) (D a :** a)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term d g2 a
y)

-- | 'cut' with the producer first, as System L writes @⟨t | k⟩@: @t |> k@ sends @t@ into @k@.
(|>)
  :: forall {k} (a :: SYN k) d g1 g2
   . (StarAutonomous k, KnownObj a, Merge g2 g1)
  => Term d g1 a %1 -> Consumer d g2 a %1 -> Command d (Union g2 g1)
Term d g1 a
t |> :: forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g2 g1) =>
Term d g1 a %1 -> Consumer d g2 a %1 -> Command d (Union g2 g1)
|> Consumer d g2 a
k = Consumer d g2 a %1 -> Term d g1 a %1 -> Term d (Union g2 g1) (D I)
forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
cut Consumer d g2 a
k Term d g1 a
t

-- | Bind an input: a pattern for an @a@, as for 'toSMC', whose variables the command must use
-- exactly once, gives a consumer of @a@. As logic, this refutes @a@.
accept
  :: forall {k} d r (a :: SYN k) t cont
   . (StarAutonomous k, Binds t d a cont r (D I))
  => (t %1 -> cont)
  %1 -> Consumer d r a
accept :: forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) t cont.
(StarAutonomous k, Binds t d a cont r (D I)) =>
(t %1 -> cont) %1 -> Consumer d r a
accept t %1 -> cont
k = case forall (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
Binds t d a cont r b =>
(t %1 -> cont) %1 -> Term (d + 1) ('(d, a) : r) b
bound @d @r @a @(D I) t %1 -> cont
k of MkTerm Interp (Mul ('(d, a) : r)) ~> Interp (D I)
body -> (Interp (Mul r) ~> Interp (D a)) -> Consumer d r a
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall {k} (x :: SYN k) (r :: Ctx k).
(StarAutonomous k, KnownObj x, KnownCtx r) =>
((Interp (Mul r) ** Interp x) ~> Dual Unit)
-> Interp (Mul r) ~> Dual (Interp x)
forall (x :: SYN k) (r :: Ctx k).
(StarAutonomous k, KnownObj x, KnownCtx r) =>
((Interp (Mul r) ** Interp x) ~> Dual Unit)
-> Interp (Mul r) ~> Dual (Interp x)
consumeRight @a @r (Interp (Mul ('(d, a) : r)) ~> Dual Unit
Interp (Mul ('(d, a) : r)) ~> Interp (D I)
body (Interp (Mul ('(d, a) : r)) ~> Dual Unit)
-> ((Interp (Mul r) ** Interp a) ~> Interp (Mul ('(d, a) : r)))
-> (Interp (Mul r) ** Interp a) ~> Dual Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc @d @a @r))

-- | What 'accept' and 'par' share: a command on a context with @x@ on its right, as a consumer of
-- @x@.
consumeRight
  :: forall {k} (x :: SYN k) r
   . (StarAutonomous k, KnownObj x, KnownCtx r)
  => (Interp (Mul r) ** Interp x ~> Dual Unit) -> Interp (Mul r) ~> Dual (Interp x)
consumeRight :: forall {k} (x :: SYN k) (r :: Ctx k).
(StarAutonomous k, KnownObj x, KnownCtx r) =>
((Interp (Mul r) ** Interp x) ~> Dual Unit)
-> Interp (Mul r) ~> Dual (Interp x)
consumeRight (Interp (Mul r) ** Interp x) ~> Dual Unit
f =
  forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @r (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @x ((Interp x ~> (Interp x ** Unit))
-> Dual (Interp x ** Unit) ~> Dual (Interp x)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
dual (forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @k @(Interp x)) (Dual (Interp x ** Unit) ~> Dual (Interp x))
-> (Interp (Mul r) ~> Dual (Interp x ** Unit))
-> Interp (Mul r) ~> Dual (Interp x)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @k @(Interp (Mul r)) @(Interp x) @Unit (Interp (Mul r) ** Interp x) ~> Dual Unit
f))

-- | Bind an output: a consumer of @a@, which the command must use exactly once, gives a producer of
-- @a@. As logic, this is proof by contradiction, and in Haskell it is @callCC@: 'doubleNeg' after
-- 'accept'.
emit
  :: forall {k} d r (a :: SYN k) da
   . (StarAutonomous k, KnownObj a, KnownCtx r)
  => (Consumer da '[ '(d, D a)] a %1 -> Command (d + 1) ('(d, D a) ': r))
  %1 -> Term d r a
emit :: forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (da :: Nat).
(StarAutonomous k, KnownObj a, KnownCtx r) =>
(Consumer da '[ '(d, D a)] a %1 -> Command (d + 1) ('(d, D a) : r))
%1 -> Term d r a
emit Consumer da '[ '(d, D a)] a %1 -> Command (d + 1) ('(d, D a) : r)
k = case forall (d :: Nat) (r :: Ctx k) (a :: SYN k) t cont.
(StarAutonomous k, Binds t d a cont r (D I)) =>
(t %1 -> cont) %1 -> Consumer d r a
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) t cont.
(StarAutonomous k, Binds t d a cont r (D I)) =>
(t %1 -> cont) %1 -> Consumer d r a
accept @d @r @(D a) Consumer da '[ '(d, D a)] a %1 -> Command (d + 1) ('(d, D a) : r)
k of
  MkTerm Interp (Mul r) ~> Interp (D (D a))
t -> forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a ((Interp (Mul r) ~> Interp a) -> Term d r a
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall k (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @k @(Interp a) (Dual (Dual (Interp a)) ~> Interp a)
-> (Interp (Mul r) ~> Dual (Dual (Interp a)))
-> Interp (Mul r) ~> Interp a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Interp (Mul r) ~> Dual (Dual (Interp a))
Interp (Mul r) ~> Interp (D (D a))
t))

-- | Bind two outputs: consumers of @a@ and of @b@, which the command must use exactly once each,
-- give a producer of their par.
par
  :: forall {k} d r (a :: SYN k) b da db
   . (StarAutonomous k, KnownObj a, KnownObj b, KnownCtx r)
  => ( Consumer da '[ '(d, D a)] a
       %1 -> Consumer db '[ '(d + 1, D b)] b
       %1 -> Command (d + 2) ('(d + 1, D b) ': '(d, D a) ': r)
     )
  %1 -> Term d r (a :## b)
par :: forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k)
       (da :: Nat) (db :: Nat).
(StarAutonomous k, KnownObj a, KnownObj b, KnownCtx r) =>
(Consumer da '[ '(d, D a)] a
 %1 -> Consumer db '[ '(d + 1, D b)] b
 %1 -> Command (d + 2) ('(d + 1, D b) : '(d, D a) : r))
%1 -> Term d r (a :## b)
par Consumer da '[ '(d, D a)] a
%1 -> Consumer db '[ '(d + 1, D b)] b
%1 -> Command (d + 2) ('(d + 1, D b) : '(d, D a) : r)
k = case Consumer da '[ '(d, D a)] a
%1 -> Consumer db '[ '(d + 1, D b)] b
%1 -> Command (d + 2) ('(d + 1, D b) : '(d, D a) : r)
k (forall (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
forall {k} (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
var @d @(D a)) (forall (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
forall {k} (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
var @(d + 1) @(D b)) of
  MkTerm Interp (Mul ('(d + 1, D b) : '(d, D a) : r)) ~> Interp (D I)
body -> (Interp (Mul r) ~> Interp (a :## b)) -> Term d r (a :## b)
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall {k} (x :: SYN k) (r :: Ctx k).
(StarAutonomous k, KnownObj x, KnownCtx r) =>
((Interp (Mul r) ** Interp x) ~> Dual Unit)
-> Interp (Mul r) ~> Dual (Interp x)
forall (x :: SYN k) (r :: Ctx k).
(StarAutonomous k, KnownObj x, KnownCtx r) =>
((Interp (Mul r) ** Interp x) ~> Dual Unit)
-> Interp (Mul r) ~> Dual (Interp x)
consumeRight @(D a :** D b) @r ((Interp (Mul ('(d, D a) : r)) ** Dual (Interp b)) ~> Dual Unit
Interp (Mul ('(d + 1, D b) : '(d, D a) : r)) ~> Interp (D I)
body ((Interp (Mul ('(d, D a) : r)) ** Dual (Interp b)) ~> Dual Unit)
-> ((Interp (Mul r) ** (Dual (Interp a) ** Dual (Interp b)))
    ~> (Interp (Mul ('(d, D a) : r)) ** Dual (Interp b)))
-> (Interp (Mul r) ** (Dual (Interp a) ** Dual (Interp b)))
   ~> Dual Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) (a :: SYN k) (m :: Nat) (b :: SYN k)
       (g :: Ctx k).
(Monoidal k, KnownObj a, KnownObj b, KnownCtx g) =>
(Interp (Mul g) ** (Interp a ** Interp b))
~> Interp (Mul ('(m, b) : '(n, a) : g))
forall {k} (n :: Nat) (a :: SYN k) (m :: Nat) (b :: SYN k)
       (g :: Ctx k).
(Monoidal k, KnownObj a, KnownObj b, KnownCtx g) =>
(Interp (Mul g) ** (Interp a ** Interp b))
~> Interp (Mul ('(m, b) : '(n, a) : g))
snoc2 @d @(D a) @(d + 1) @(D b) @r))

-- | A consumer of a par from a consumer of each side. Cutting the par against the tensor of the two
-- consumers does the same with less structure.
both
  :: forall {k} d g1 g2 (a :: SYN k) b
   . (StarAutonomous k, KnownObj a, KnownObj b, Merge g1 g2)
  => Consumer d g1 a %1 -> Consumer d g2 b %1 -> Consumer d (Union g1 g2) (a :## b)
both :: forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(StarAutonomous k, KnownObj a, KnownObj b, Merge g1 g2) =>
Consumer d g1 a
%1 -> Consumer d g2 b %1 -> Consumer d (Union g1 g2) (a :## b)
both Consumer d g1 a
x Consumer d g2 b
y = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(D a :** D b) @(D (a :## b)) (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @(D a :** D b) (forall k (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @k @(Interp (D a :** D b)))) (Consumer d g1 a
x Consumer d g1 a
%1 -> Consumer d g2 b %1 -> Term d (Union g1 g2) (D a :** D b)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Consumer d g2 b
y)

-- $additives
-- The additives share their context between alternatives, of which only one is used. Terms that
-- share variables can't both be written in a linear function, so the alternatives are functions of
-- their own, compiled with 'toSMC' like the argument of 'call', and what they share is passed in as
-- one term.

-- | Both of two alternatives on the same input: the product. Each alternative takes the input with
-- a pattern, as for 'toSMC'. This needs products.
with
  :: forall {k} (s :: SYN k) a b d g t1 cont1 t2 cont2
   . (Monoidal k, HasBinaryProducts k, Binds t1 0 s cont1 '[] a, Binds t2 0 s cont2 '[] b)
  => (t1 %1 -> cont1)
  -> (t2 %1 -> cont2)
  -> Term d g s
  %1 -> Term d g (a :&& b)
with :: forall {k} (s :: SYN k) (a :: SYN k) (b :: SYN k) (d :: Nat)
       (g :: Ctx k) t1 cont1 t2 cont2.
(Monoidal k, HasBinaryProducts k, Binds t1 0 s cont1 '[] a,
 Binds t2 0 s cont2 '[] b) =>
(t1 %1 -> cont1)
-> (t2 %1 -> cont2) -> Term d g s %1 -> Term d g (a :&& b)
with t1 %1 -> cont1
f t2 %1 -> cont2
h = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @s @(a :&& b) (forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @s @a t1 %1 -> cont1
f (Interp s ~> Interp a)
-> (Interp s ~> Interp b) -> Interp s ~> (Interp a && Interp 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)
&&& forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @s @b t2 %1 -> cont2
h)

-- | The first alternative of a product.
exl
  :: forall {k} (a :: SYN k) b d g. (HasBinaryProducts k, KnownObj a, KnownObj b) => Term d g (a :&& b) %1 -> Term d g a
exl :: forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
(HasBinaryProducts k, KnownObj a, KnownObj b) =>
Term d g (a :&& b) %1 -> Term d g a
exl = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(a :&& b) @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @(Interp a) @(Interp b))))

-- | The second alternative of a product.
exr
  :: forall {k} (a :: SYN k) b d g. (HasBinaryProducts k, KnownObj a, KnownObj b) => Term d g (a :&& b) %1 -> Term d g b
exr :: forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
(HasBinaryProducts k, KnownObj a, KnownObj b) =>
Term d g (a :&& b) %1 -> Term d g b
exr = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(a :&& b) @b (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @(Interp a) @(Interp b))))

-- | Use up a term into the unit of the product.
absorb :: forall {k} (s :: SYN k) d g. (HasTerminalObject k, KnownObj s) => Term d g s %1 -> Term d g Top
absorb :: forall {k} (s :: SYN k) (d :: Nat) (g :: Ctx k).
(HasTerminalObject k, KnownObj s) =>
Term d g s %1 -> Term d g Top
absorb = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @s @Top (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @s (forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @k @(Interp s)))

-- | The left injection into a coproduct.
inl
  :: forall {k} (a :: SYN k) b d g
   . (HasBinaryCoproducts k, KnownObj a, KnownObj b)
  => Term d g a %1 -> Term d g (a :|| b)
inl :: forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
(HasBinaryCoproducts k, KnownObj a, KnownObj b) =>
Term d g a %1 -> Term d g (a :|| b)
inl = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @a @(a :|| b) (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @(Interp a) @(Interp b))))

-- | The right injection into a coproduct.
inr
  :: forall {k} (a :: SYN k) b d g
   . (HasBinaryCoproducts k, KnownObj a, KnownObj b)
  => Term d g b %1 -> Term d g (a :|| b)
inr :: forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
(HasBinaryCoproducts k, KnownObj a, KnownObj b) =>
Term d g b %1 -> Term d g (a :|| b)
inr = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @b @(a :|| b) (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @(Interp a) @(Interp b))))

-- | Case analysis on a coproduct, given first a term to share between the branches. Both branches
-- take the pair of the shared term and the contents of their alternative with a pattern, as for
-- 'toSMC'. This needs the tensor to distribute over the coproduct.
caseOf
  :: forall {k} (s :: SYN k) a b c d g1 g2 t1 cont1 t2 cont2
   . ( Distributive k
     , KnownObj s
     , KnownObj a
     , KnownObj b
     , Merge g1 g2
     , Binds t1 0 (s :** a) cont1 '[] c
     , Binds t2 0 (s :** b) cont2 '[] c
     )
  => Term d g1 s
  %1 -> Term d g2 (a :|| b)
  %1 -> (t1 %1 -> cont1)
  -> (t2 %1 -> cont2)
  -> Term d (Union g1 g2) c
caseOf :: forall {k} (s :: SYN k) (a :: SYN k) (b :: SYN k) (c :: SYN k)
       (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) t1 cont1 t2 cont2.
(Distributive k, KnownObj s, KnownObj a, KnownObj b, Merge g1 g2,
 Binds t1 0 (s :** a) cont1 '[] c,
 Binds t2 0 (s :** b) cont2 '[] c) =>
Term d g1 s
%1 -> Term d g2 (a :|| b)
%1 -> (t1 %1 -> cont1)
-> (t2 %1 -> cont2)
-> Term d (Union g1 g2) c
caseOf Term d g1 s
e Term d g2 (a :|| b)
x t1 %1 -> cont1
f t2 %1 -> cont2
h =
  forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(s :** (a :|| b)) @c
    ( forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @s
        ( forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a
            ( forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b
                ( (forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(s :** a) @c t1 %1 -> cont1
f ((Interp s ** Interp a) ~> Interp c)
-> ((Interp s ** Interp b) ~> Interp c)
-> ((Interp s ** Interp a) || (Interp s ** Interp b)) ~> Interp c
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
||| forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(s :** b) @c t2 %1 -> cont2
h)
                    (((Interp s ** Interp a) || (Interp s ** Interp b)) ~> Interp c)
-> ((Interp s ** (Interp a || Interp b))
    ~> ((Interp s ** Interp a) || (Interp s ** Interp b)))
-> (Interp s ** (Interp a || Interp b)) ~> Interp c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p 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 @k @(Interp s) @(Interp a) @(Interp b)
                )
            )
        )
    )
    (Term d g1 s
e Term d g1 s
%1 -> Term d g2 (a :|| b)
%1 -> Term d (Union g1 g2) (s :** (a :|| b))
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term d g2 (a :|| b)
x)

-- | There is no term of 'Zero', so from one, together with the rest of the context, anything
-- follows.
absurd
  :: forall {k} (s :: SYN k) c d g1 g2
   . (Distributive k, KnownObj s, KnownObj c, Merge g1 g2)
  => Term d g1 s %1 -> Term d g2 Zero %1 -> Term d (Union g1 g2) c
absurd :: forall {k} (s :: SYN k) (c :: SYN k) (d :: Nat) (g1 :: Ctx k)
       (g2 :: Ctx k).
(Distributive k, KnownObj s, KnownObj c, Merge g1 g2) =>
Term d g1 s %1 -> Term d g2 Zero %1 -> Term d (Union g1 g2) c
absurd Term d g1 s
e Term d g2 Zero
z = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(s :** Zero) @c (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @s (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @c (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @k @(Interp c) (InitialObject ~> Interp c)
-> ((Interp s ** InitialObject) ~> InitialObject)
-> (Interp s ** InitialObject) ~> Interp c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
absorbL @k @(Interp s)))) (Term d g1 s
e Term d g1 s
%1 -> Term d g2 Zero %1 -> Term d (Union g1 g2) (s :** Zero)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term d g2 Zero
z)

-- | Function application. The function and its argument must have disjoint contexts.
(!)
  :: forall {k} d g1 g2 (a :: SYN k) b
   . (Closed k, KnownObj a, KnownObj b, Merge g1 g2)
  => Term d g1 (a :-> b) %1 -> Term d g2 a %1 -> Term d (Union g1 g2) b
MkTerm Interp (Mul g1) ~> Interp (a :-> b)
f ! :: forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Closed k, KnownObj a, KnownObj b, Merge g1 g2) =>
Term d g1 (a :-> b) %1 -> Term d g2 a %1 -> Term d (Union g1 g2) b
! MkTerm Interp (Mul g2) ~> Interp a
x =
  forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @b ((Interp (Mul (Union g1 g2)) ~> Interp b) -> Term d (Union g1 g2) b
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @(Interp a) @(Interp b) (((Interp a ~~> Interp b) ** Interp a) ~> Interp b)
-> (Interp (Mul (Union g1 g2))
    ~> ((Interp a ~~> Interp b) ** Interp a))
-> Interp (Mul (Union g1 g2)) ~> Interp b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Interp (Mul g1) ~> (Interp a ~~> Interp b)
Interp (Mul g1) ~> Interp (a :-> b)
f (Interp (Mul g1) ~> (Interp a ~~> Interp b))
-> (Interp (Mul g2) ~> Interp a)
-> (Interp (Mul g1) ** Interp (Mul g2))
   ~> ((Interp a ~~> Interp b) ** Interp a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Interp (Mul g2) ~> Interp a
x) ((Interp (Mul g1) ** Interp (Mul g2))
 ~> ((Interp a ~~> Interp b) ** Interp a))
-> (Interp (Mul (Union g1 g2))
    ~> (Interp (Mul g1) ** Interp (Mul g2)))
-> Interp (Mul (Union g1 g2))
   ~> ((Interp a ~~> Interp b) ** Interp a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @g1 @g2)))

-- Do notation

-- | The pattern @t@ of a binder: it takes apart the variable @(n, a)@, and the binder's body
-- @cont@ then gives a term at depth @n + 1@ with type @b@, whose context is that variable and @g@.
-- Both the variable's type and the rest of the context must be known.
type Binds :: forall k. Type -> Nat -> SYN k -> Type -> Ctx k -> SYN k -> Constraint
type Binds @k t n a cont g b =
  (KnownObj a, KnownCtx g, Bind k (Term (n + 1) '[ '(n, a)] a) t One cont (Term (n + 1) ('(n, a) ': g) b))

-- | A bind in a @do@ block: a term taken apart by a pattern, or the variables of a @rec@ block.
-- The multiplicity @p@ of the continuation depends only on the right hand side @m@, since GHC
-- needs it before it knows the rest.
type Bind :: Type -> Type -> Type -> Multiplicity -> Type -> Type -> Constraint
class Bind k m t p cont r | m -> k p where
  -- | Bind the right hand side to the pattern of the continuation.
  (>>=) :: m %1 -> (t %p -> cont) %1 -> r

-- The types of the continuation and the result are matched with equalities, so that the
-- instance is chosen as soon as the right hand side is known.
instance
  {-# INCOHERENT #-}
  ( cont ~ Term (d + PSize t) (CtxOf @k cont) (TyOf @k cont)
  , r ~ Term d (PCtx t d g a (CtxOf @k cont)) (TyOf @k cont)
  , Pat k t d g a (CtxOf @k cont) (TyOf @k cont)
  )
  => Bind k (Term d g (a :: SYN k)) t One cont r
  where
  >>= :: Term d g a %1 -> (t %1 -> cont) %1 -> r
(>>=) = forall k t (d :: Nat) (g :: Ctx k) (a :: SYN k) (g' :: Ctx k)
       (c :: SYN k).
Pat k t d g a g' c =>
Term d g a
%1 -> (t %1 -> Term (d + PSize t) g' c)
%1 -> Term d (PCtx t d g a g') c
pat @k @t @d @g @a @(CtxOf @k cont) @(TyOf @k cont)

-- | The statement of a @rec@ block, whose continuation is its 'return'.
instance
  (Bind k (Term d g a) t One cont r', r ~ Ret tt r')
  => Bind k (Term d g (a :: SYN k)) t One (Ret tt cont) r
  where
  Term d g a
x >>= :: Term d g a %1 -> (t %1 -> Ret tt cont) %1 -> r
>>= t %1 -> Ret tt cont
k = r' -> Ret tt r'
forall t x. x -> Ret t x
Ret (Term d g a
x Term d g a %1 -> (t %1 -> cont) %1 -> r'
forall k m t (p :: Multiplicity) cont r.
Bind k m t p cont r =>
m %1 -> (t %p -> cont) %1 -> r
>>= \t
p -> Ret tt cont %1 -> cont
forall t x. Ret t x %1 -> x
unRet (t %1 -> Ret tt cont
k t
p))

-- | The body of a @rec@ block, tagged with the tuple of its variables. GHC's translation passes
-- that tuple to both 'return' and 'mfix', and this tag is what makes them the same.
type Ret :: Type -> Type -> Type
newtype Ret t x = Ret x

unRet :: Ret t x %1 -> x
unRet :: forall t x. Ret t x %1 -> x
unRet (Ret x
x) = x
x

-- | A pattern: a variable, @()@, or a pair of patterns. A triple or quadruple stands for pairs
-- nested to the left, as @a ':**' b ':**' c@ is: @(x, y, z)@ is @((x, y), z)@. Binding it at depth
-- @d@ to a term with context @g@ and type @a@, with a continuation with context @g'@ and type @c@.
type Pat :: forall k -> Type -> Nat -> Ctx k -> SYN k -> Ctx k -> SYN k -> Constraint
class Pat k t d g a g' c where
  pat :: Term d g a %1 -> (t %1 -> Term (d + PSize t) g' c) %1 -> Term d (PCtx t d g a g') c

-- | The number of variables a pattern binds on the way, and so the depth it adds.
type PSize :: Type -> Nat
type family PSize t where
  PSize (x, y) = 2 + PSize x + PSize y
  PSize (x, y, z) = PSize ((x, y), z)
  PSize (w, x, y, z) = PSize (((w, x), y), z)
  PSize t = 0

-- | The context of a pattern match, from the context of the right hand side and of the
-- continuation.
type PCtx :: forall {k}. Type -> Nat -> Ctx k -> SYN k -> Ctx k -> Ctx k
type family PCtx t d g a g' where
  PCtx (x, y) d g (a1 :** a2) g' = Union (Drop2 (PCtxPair x y d a1 a2 g')) g
  PCtx (x, y, z) d g a g' = PCtx ((x, y), z) d g a g'
  PCtx (w, x, y, z) d g a g' = PCtx (((w, x), y), z) d g a g'
  PCtx () d g a g' = Union g g'
  PCtx t d g a g' = g'

-- | The context of the body of the 'split' that a pair pattern starts with.
type PCtxPair :: forall {k}. Type -> Type -> Nat -> SYN k -> SYN k -> Ctx k -> Ctx k
type PCtxPair x y d a1 a2 g' =
  PCtx x (d + 2) '[ '(d, a1)] a1 (PCtx y (d + 2 + PSize x) '[ '(d + 1, a2)] a2 g')

-- Both instances are incoherent: a variable pattern's type is often still unknown when the
-- instance is chosen, and a pair pattern's type is always a pair by then.

-- | The pattern @()@ uses up a term of the unit type.
instance {-# INCOHERENT #-} (Monoidal k, a ~ I, KnownObj c, Merge g g') => Pat k () d g (a :: SYN k) g' c where
  pat :: Term d g a
%1 -> (() %1 -> Term (d + PSize ()) g' c)
%1 -> Term d (PCtx () d g a g') c
pat (MkTerm Interp (Mul g) ~> Interp a
u) () %1 -> Term (d + PSize ()) g' c
k = case () %1 -> Term (d + PSize ()) g' c
k () of
    MkTerm Interp (Mul g') ~> Interp c
t -> forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @c ((Interp (Mul (Union g g')) ~> Interp c) -> Term d (Union g g') c
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @(Interp c) ((Unit ** Interp c) ~> Interp c)
-> (Interp (Mul (Union g g')) ~> (Unit ** Interp c))
-> Interp (Mul (Union g g')) ~> Interp c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Interp (Mul g) ~> Unit
Interp (Mul g) ~> Interp a
u (Interp (Mul g) ~> Unit)
-> (Interp (Mul g') ~> Interp c)
-> (Interp (Mul g) ** Interp (Mul g')) ~> (Unit ** Interp c)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Interp (Mul g') ~> Interp c
t) ((Interp (Mul g) ** Interp (Mul g')) ~> (Unit ** Interp c))
-> (Interp (Mul (Union g g'))
    ~> (Interp (Mul g) ** Interp (Mul g')))
-> Interp (Mul (Union g g')) ~> (Unit ** Interp c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @g @g'))

instance {-# INCOHERENT #-} (t ~ Term (DepthOf t) g a) => Pat k t d g a g' c where
  pat :: Term d g a
%1 -> (t %1 -> Term (d + PSize t) g' c)
%1 -> Term d (PCtx t d g a g') c
pat Term d g a
x t %1 -> Term (d + PSize t) g' c
k = t %1 -> Term (d + PSize t) g' c
k (Term d g a %1 -> Term (DepthOf t) g a
forall {k} (d :: Nat) (g :: Ctx k) (a :: SYN k) (d' :: Nat).
Term d g a %1 -> Term d' g a
retag Term d g a
x)

instance
  {-# INCOHERENT #-}
  ( Monoidal k
  , a ~ (a1 :** a2)
  , KnownObj a1
  , KnownObj a2
  , Pat k x (d + 2) '[ '(d, a1)] a1 (PCtx y (d + 2 + PSize x) '[ '(d + 1, a2)] a2 g') c
  , Pat k y (d + 2 + PSize x) '[ '(d + 1, a2)] a2 g' c
  , d + 2 + PSize x + PSize y ~ d + PSize (x, y)
  , PCtxPair x y d a1 a2 g' ~ ('(d + 1, a2) ': '(d, a1) ': Drop2 (PCtxPair x y d a1 a2 g'))
  , Merge (Drop2 (PCtxPair x y d a1 a2 g')) g
  )
  => Pat k (x, y) d g (a :: SYN k) g' c
  where
  pat :: Term d g a
%1 -> ((x, y) %1 -> Term (d + PSize (x, y)) g' c)
%1 -> Term d (PCtx (x, y) d g a g') c
pat Term d g a
s (x, y) %1 -> Term (d + PSize (x, y)) g' c
k =
    Term d g (a1 :** a2)
%1 -> (Term (d + 2) '[ '(d, a1)] a1
       %1 -> Term ((d + 2) + PSize x) '[ '(d + 1, a2)] a2
       %1 -> Term
               (d + 2)
               ('(d + 1, a2) : '(d, a1) : Drop2 (PCtxPair x y d a1 a2 g'))
               c)
%1 -> Term d (Union (Drop2 (PCtxPair x y d a1 a2 g')) g) c
forall {k} (d :: Nat) (g :: Ctx k) (r :: Ctx k) (a :: SYN k)
       (b :: SYN k) (c :: SYN k) (da :: Nat) (db :: Nat).
(Monoidal k, KnownObj a, KnownObj b, Merge r g) =>
Term d g (a :** b)
%1 -> (Term da '[ '(d, a)] a
       %1 -> Term db '[ '(d + 1, b)] b
       %1 -> Term (d + 2) ('(d + 1, b) : '(d, a) : r) c)
%1 -> Term d (Union r g) c
split
      Term d g a
Term d g (a1 :** a2)
s
      ( \Term (d + 2) '[ '(d, a1)] a1
a Term ((d + 2) + PSize x) '[ '(d + 1, a2)] a2
b ->
          forall k t (d :: Nat) (g :: Ctx k) (a :: SYN k) (g' :: Ctx k)
       (c :: SYN k).
Pat k t d g a g' c =>
Term d g a
%1 -> (t %1 -> Term (d + PSize t) g' c)
%1 -> Term d (PCtx t d g a g') c
pat @k @x @(d + 2) @'[ '(d, a1)] @a1 @(PCtx y (d + 2 + PSize x) '[ '(d + 1, a2)] a2 g') @c
            Term (d + 2) '[ '(d, a1)] a1
a
            (\x
px -> forall k t (d :: Nat) (g :: Ctx k) (a :: SYN k) (g' :: Ctx k)
       (c :: SYN k).
Pat k t d g a g' c =>
Term d g a
%1 -> (t %1 -> Term (d + PSize t) g' c)
%1 -> Term d (PCtx t d g a g') c
pat @k @y @(d + 2 + PSize x) @'[ '(d + 1, a2)] @a2 @g' @c Term ((d + 2) + PSize x) '[ '(d + 1, a2)] a2
b (\y
py -> (x, y) %1 -> Term (d + PSize (x, y)) g' c
k (x
px, y
py)))
      )

instance {-# INCOHERENT #-} (Pat k ((x, y), z) d g a g' c) => Pat k (x, y, z) d g a g' c where
  pat :: Term d g a
%1 -> ((x, y, z) %1 -> Term (d + PSize (x, y, z)) g' c)
%1 -> Term d (PCtx (x, y, z) d g a g') c
pat Term d g a
s (x, y, z) %1 -> Term (d + PSize (x, y, z)) g' c
k = forall k t (d :: Nat) (g :: Ctx k) (a :: SYN k) (g' :: Ctx k)
       (c :: SYN k).
Pat k t d g a g' c =>
Term d g a
%1 -> (t %1 -> Term (d + PSize t) g' c)
%1 -> Term d (PCtx t d g a g') c
pat @k @((x, y), z) @d @g @a @g' @c Term d g a
s (\((x
px, y
py), z
pz) -> (x, y, z) %1 -> Term (d + PSize (x, y, z)) g' c
k (x
px, y
py, z
pz))

instance {-# INCOHERENT #-} (Pat k (((w, x), y), z) d g a g' c) => Pat k (w, x, y, z) d g a g' c where
  pat :: Term d g a
%1 -> ((w, x, y, z) %1 -> Term (d + PSize (w, x, y, z)) g' c)
%1 -> Term d (PCtx (w, x, y, z) d g a g') c
pat Term d g a
s (w, x, y, z) %1 -> Term (d + PSize (w, x, y, z)) g' c
k = forall k t (d :: Nat) (g :: Ctx k) (a :: SYN k) (g' :: Ctx k)
       (c :: SYN k).
Pat k t d g a g' c =>
Term d g a
%1 -> (t %1 -> Term (d + PSize t) g' c)
%1 -> Term d (PCtx t d g a g') c
pat @k @(((w, x), y), z) @d @g @a @g' @c Term d g a
s (\(((w
pw, x
px), y
py), z
pz) -> (w, x, y, z) %1 -> Term (d + PSize (w, x, y, z)) g' c
k (w
pw, x
px, y
py, z
pz))

-- | The variables of a @rec@ block, as GHC tuples them up.
type RecVars :: Type -> Type -> Constraint
class RecVars k t | t -> k where
  type Vars k t :: Ctx k
  recVars :: t
  consume :: t %1 -> r %1 -> r

instance (Monoidal k, KnownObj (a :: SYN k)) => RecVars k (Term d '[ '(n, a)] a) where
  type Vars k (Term d '[ '(n, a)] a) = '[ '(n, a)]
  recVars :: Term d '[ '(n, a)] a
recVars = forall (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
forall {k} (n :: Nat) (a :: SYN k) (d :: Nat).
(CategoryOf k, KnownObj a) =>
Term d '[ '(n, a)] a
var @n @a
  consume :: forall r. Term d '[ '(n, a)] a %1 -> r %1 -> r
consume (MkTerm Interp (Mul '[ '(n, a)]) ~> Interp a
_) r
r = r
r

instance (RecVars k x, RecVars k y) => RecVars k (x, y) where
  type Vars k (x, y) = Union (Vars k x) (Vars k y)
  recVars :: (x, y)
recVars = (x
forall k t. RecVars k t => t
recVars, y
forall k t. RecVars k t => t
recVars)
  consume :: forall r. (x, y) %1 -> r %1 -> r
consume (x
x, y
y) r
r = x %1 -> r %1 -> r
forall r. x %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume x
x (y %1 -> r %1 -> r
forall r. y %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume y
y r
r)

instance (RecVars k x, RecVars k y, RecVars k z) => RecVars k (x, y, z) where
  type Vars k (x, y, z) = Union (Vars k x) (Vars k (y, z))
  recVars :: (x, y, z)
recVars = (x
forall k t. RecVars k t => t
recVars, y
forall k t. RecVars k t => t
recVars, z
forall k t. RecVars k t => t
recVars)
  consume :: forall r. (x, y, z) %1 -> r %1 -> r
consume (x
x, y
y, z
z) r
r = x %1 -> r %1 -> r
forall r. x %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume x
x ((y, z) %1 -> r %1 -> r
forall r. (y, z) %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume (y
y, z
z) r
r)

instance (RecVars k x, RecVars k y, RecVars k z, RecVars k w) => RecVars k (x, y, z, w) where
  type Vars k (x, y, z, w) = Union (Vars k x) (Vars k (y, z, w))
  recVars :: (x, y, z, w)
recVars = (x
forall k t. RecVars k t => t
recVars, y
forall k t. RecVars k t => t
recVars, z
forall k t. RecVars k t => t
recVars, w
forall k t. RecVars k t => t
recVars)
  consume :: forall r. (x, y, z, w) %1 -> r %1 -> r
consume (x
x, y
y, z
z, w
w) r
r = x %1 -> r %1 -> r
forall r. x %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume x
x ((y, z, w) %1 -> r %1 -> r
forall r. (y, z, w) %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume (y
y, z
z, w
w) r
r)

instance (RecVars k x, RecVars k y, RecVars k z, RecVars k w, RecVars k v) => RecVars k (x, y, z, w, v) where
  type Vars k (x, y, z, w, v) = Union (Vars k x) (Vars k (y, z, w, v))
  recVars :: (x, y, z, w, v)
recVars = (x
forall k t. RecVars k t => t
recVars, y
forall k t. RecVars k t => t
recVars, z
forall k t. RecVars k t => t
recVars, w
forall k t. RecVars k t => t
recVars, v
forall k t. RecVars k t => t
recVars)
  consume :: forall r. (x, y, z, w, v) %1 -> r %1 -> r
consume (x
x, y
y, z
z, w
w, v
v) r
r = x %1 -> r %1 -> r
forall r. x %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume x
x ((y, z, w, v) %1 -> r %1 -> r
forall r. (y, z, w, v) %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume (y
y, z
z, w
w, v
v) r
r)

instance
  (RecVars k x, RecVars k y, RecVars k z, RecVars k w, RecVars k v, RecVars k u)
  => RecVars k (x, y, z, w, v, u)
  where
  type Vars k (x, y, z, w, v, u) = Union (Vars k x) (Vars k (y, z, w, v, u))
  recVars :: (x, y, z, w, v, u)
recVars = (x
forall k t. RecVars k t => t
recVars, y
forall k t. RecVars k t => t
recVars, z
forall k t. RecVars k t => t
recVars, w
forall k t. RecVars k t => t
recVars, v
forall k t. RecVars k t => t
recVars, u
forall k t. RecVars k t => t
recVars)
  consume :: forall r. (x, y, z, w, v, u) %1 -> r %1 -> r
consume (x
x, y
y, z
z, w
w, v
v, u
u) r
r = x %1 -> r %1 -> r
forall r. x %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume x
x ((y, z, w, v, u) %1 -> r %1 -> r
forall r. (y, z, w, v, u) %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume (y
y, z
z, w
w, v
v, u
u) r
r)

-- | The end of a @rec@ block: all its variables, as the tensor of their context.
return
  :: forall k t d. (Monoidal k, RecVars k t, KnownCtx (Vars k t)) => t %1 -> Ret t (Term d (Vars k t) (Mul (Vars k t)))
return :: forall k t (d :: Nat).
(Monoidal k, RecVars k t, KnownCtx (Vars k t)) =>
t %1 -> Ret t (Term d (Vars k t) (Mul (Vars k t)))
return t
t = Term d (Vars k t) (Mul (Vars k t))
-> Ret t (Term d (Vars k t) (Mul (Vars k t)))
forall t x. x -> Ret t x
Ret (t
%1 -> Term d (Vars k t) (Mul (Vars k t))
%1 -> Term d (Vars k t) (Mul (Vars k t))
forall r. t %1 -> r %1 -> r
forall k t r. RecVars k t => t %1 -> r %1 -> r
consume t
t ((Interp (Mul (Vars k t)) ~> Interp (Mul (Vars k t)))
-> Term d (Vars k t) (Mul (Vars k t))
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @(Vars k t))))

-- | A @rec@ block after tracing, from its context without the fed back variables to the variables
-- it passes on.
type Rec :: forall {k}. Nat -> Type -> Ctx k -> Ctx k -> Type
data Rec d t g0 outs where
  Rec :: (Interp (Mul g0) ~> Interp (Mul outs)) %Many -> Rec d t g0 outs

-- | Trace a @rec@ block: the variables it uses before binding them are fed back.
mfix
  :: forall {k} t d (g :: Ctx k)
   . ( TracedMonoidal k
     , RecVars k t
     , Merge (Inter g (Vars k t)) (Minus g (Vars k t))
     , Merge (Inter g (Vars k t)) (Minus (Vars k t) g)
     , Union (Inter g (Vars k t)) (Minus g (Vars k t)) ~ g
     , Union (Inter g (Vars k t)) (Minus (Vars k t) g) ~ Vars k t
     )
  => (t -> Ret t (Term d g (Mul (Vars k t)))) %1 -> Rec d t (Minus g (Vars k t)) (Minus (Vars k t) g)
mfix :: forall {k} t (d :: Nat) (g :: Ctx k).
(TracedMonoidal k, RecVars k t,
 Merge (Inter g (Vars k t)) (Minus g (Vars k t)),
 Merge (Inter g (Vars k t)) (Minus (Vars k t) g),
 Union (Inter g (Vars k t)) (Minus g (Vars k t)) ~ g,
 Union (Inter g (Vars k t)) (Minus (Vars k t) g) ~ Vars k t) =>
(t -> Ret t (Term d g (Mul (Vars k t))))
%1 -> Rec d t (Minus g (Vars k t)) (Minus (Vars k t) g)
mfix t -> Ret t (Term d g (Mul (Vars k t)))
f = case Ret t (Term d g (Mul (Vars k t))) %1 -> Term d g (Mul (Vars k t))
forall t x. Ret t x %1 -> x
unRet (t -> Ret t (Term d g (Mul (Vars k t)))
f t
forall k t. RecVars k t => t
recVars) of
  MkTerm Interp (Mul g) ~> Interp (Mul (Vars k t))
body ->
    forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @(Inter g (Vars k t))
      ( forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @(Minus g (Vars k t))
          ( forall (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(Monoidal k, KnownCtx g) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @(Minus (Vars k t) g)
              ( (Interp (Mul (Minus g (Vars k t)))
 ~> Interp (Mul (Minus (Vars k t) g)))
-> Rec d t (Minus g (Vars k t)) (Minus (Vars k t) g)
forall {k} (g0 :: Ctx k) (outs :: Ctx k) (d :: Nat) t.
(Interp (Mul g0) ~> Interp (Mul outs)) -> Rec d t g0 outs
Rec
                  ( forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact
                      @Tensor
                      @(~>)
                      @(Interp (Mul (Inter g (Vars k t))))
                      @(Interp (Mul (Minus g (Vars k t))))
                      @(Interp (Mul (Minus (Vars k t) g)))
                      ( forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @(Inter g (Vars k t)) @(Minus (Vars k t) g)
                          (Interp (Mul (Vars k t))
 ~> (Interp (Mul (Inter g (Vars k t)))
     ** Interp (Mul (Minus (Vars k t) g))))
-> ((Interp (Mul (Inter g (Vars k t)))
     ** Interp (Mul (Minus g (Vars k t))))
    ~> Interp (Mul (Vars k t)))
-> (Interp (Mul (Inter g (Vars k t)))
    ** Interp (Mul (Minus g (Vars k t))))
   ~> (Interp (Mul (Inter g (Vars k t)))
       ** Interp (Mul (Minus (Vars k t) g)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Interp (Mul g) ~> Interp (Mul (Vars k t))
body
                          (Interp (Mul g) ~> Interp (Mul (Vars k t)))
-> ((Interp (Mul (Inter g (Vars k t)))
     ** Interp (Mul (Minus g (Vars k t))))
    ~> Interp (Mul g))
-> (Interp (Mul (Inter g (Vars k t)))
    ** Interp (Mul (Minus g (Vars k t))))
   ~> Interp (Mul (Vars k t))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
unmerge @(Inter g (Vars k t)) @(Minus g (Vars k t))
                      )
                  )
              )
          )
      )

-- | The rest of the @do@ block after a @rec@ block. GHC binds the variables of the block here
-- without linearity, so the context checks see to it that the ones passed on are used once and
-- the fed back ones not at all.
instance
  ( SymMonoidal k
  , RecVars k t
  , t' ~ t
  , cont ~ Term (HeadId (Vars k t) + 1) (CtxOf @k cont) (TyOf @k cont)
  , r ~ Term d (Union (Minus (CtxOf @k cont) outs) g0) (TyOf @k cont)
  , AllIn outs (CtxOf @k cont)
  , NoneIn (Minus (CtxOf @k cont) outs) (Vars k t)
  , Merge (Minus (CtxOf @k cont) outs) g0
  , Merge (Minus (CtxOf @k cont) outs) outs
  , CtxOf @k cont ~ Union (Minus (CtxOf @k cont) outs) outs
  )
  => Bind k (Rec d t (g0 :: Ctx k) outs) t' Many cont r
  where
  Rec Interp (Mul g0) ~> Interp (Mul outs)
h >>= :: Rec d t g0 outs %1 -> (t' -> cont) %1 -> r
>>= t' -> cont
k = case t' -> cont
k t'
forall k t. RecVars k t => t
recVars of
    MkTerm Interp (Mul (CtxOf cont)) ~> Interp (TyOf cont)
body ->
      (Interp (Mul (Union (Minus (CtxOf cont) outs) g0))
 ~> Interp (TyOf cont))
-> Term d (Union (Minus (CtxOf cont) outs) g0) (TyOf cont)
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm
        ( Interp (Mul (CtxOf cont)) ~> Interp (TyOf cont)
body
            (Interp (Mul (CtxOf cont)) ~> Interp (TyOf cont))
-> (Interp (Mul (Union (Minus (CtxOf cont) outs) g0))
    ~> Interp (Mul (CtxOf cont)))
-> Interp (Mul (Union (Minus (CtxOf cont) outs) g0))
   ~> Interp (TyOf cont)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
unmerge @(Minus (CtxOf @k cont) outs) @outs
            ((Interp (Mul (Minus (CtxOf cont) outs)) ** Interp (Mul outs))
 ~> Interp (Mul (CtxOf cont)))
-> (Interp (Mul (Union (Minus (CtxOf cont) outs) g0))
    ~> (Interp (Mul (Minus (CtxOf cont) outs)) ** Interp (Mul outs)))
-> Interp (Mul (Union (Minus (CtxOf cont) outs) g0))
   ~> Interp (Mul (CtxOf cont))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @(Minus (CtxOf @k cont) outs) Obj (Interp (Mul (Minus (CtxOf cont) outs)))
-> (Interp (Mul g0) ~> Interp (Mul outs))
-> (Interp (Mul (Minus (CtxOf cont) outs)) ** Interp (Mul g0))
   ~> (Interp (Mul (Minus (CtxOf cont) outs)) ** Interp (Mul outs))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Interp (Mul g0) ~> Interp (Mul outs)
h)
            ((Interp (Mul (Minus (CtxOf cont) outs)) ** Interp (Mul g0))
 ~> (Interp (Mul (Minus (CtxOf cont) outs)) ** Interp (Mul outs)))
-> (Interp (Mul (Union (Minus (CtxOf cont) outs) g0))
    ~> (Interp (Mul (Minus (CtxOf cont) outs)) ** Interp (Mul g0)))
-> Interp (Mul (Union (Minus (CtxOf cont) outs) g0))
   ~> (Interp (Mul (Minus (CtxOf cont) outs)) ** Interp (Mul outs))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @(Minus (CtxOf @k cont) outs) @g0
        )

-- | GHC's translation of @rec@ refers to @fail@, but pairs of variables always match.
fail :: a
fail :: forall a. a
fail = [Char] -> a
forall a. HasCallStack => [Char] -> a
P.error [Char]
"Proarrow.Tools.SMC.fail: a pattern did not match"

retag :: Term d g a %1 -> Term d' g a
retag :: forall {k} (d :: Nat) (g :: Ctx k) (a :: SYN k) (d' :: Nat).
Term d g a %1 -> Term d' g a
retag (MkTerm Interp (Mul g) ~> Interp a
f) = (Interp (Mul g) ~> Interp a) -> Term d' g a
forall {k} (g :: Ctx k) (a :: SYN k) (d :: Nat).
(Interp (Mul g) ~> Interp a) -> Term d g a
MkTerm Interp (Mul g) ~> Interp a
f

type DepthOf :: Type -> Nat
type family DepthOf t where
  DepthOf (Term d g a) = d

type CtxOf :: forall k. Type -> Ctx k
type family CtxOf t where
  CtxOf (Term d g a) = g

type TyOf :: forall k. Type -> SYN k
type family TyOf t where
  TyOf (Term d g a) = a

type Drop2 :: forall {k}. Ctx k -> Ctx k
type family Drop2 g where
  Drop2 (x ': y ': g) = g

type HeadId :: forall {k}. Ctx k -> Nat
type family HeadId g where
  HeadId ('(n, a) ': g) = n

-- | Every variable of the first context is in the second.
type AllIn :: forall {k}. Ctx k -> Ctx k -> Constraint
type AllIn g h = IsEmpty (Text "Proarrow.Tools.SMC: a variable bound in a rec block is not used") (Minus g h)

-- | No variable of the first context is in the second.
type NoneIn :: forall {k}. Ctx k -> Ctx k -> Constraint
type NoneIn g h =
  IsEmpty (Text "Proarrow.Tools.SMC: a variable fed back in a rec block is also used after it") (Inter g h)

type IsEmpty :: forall {k}. ErrorMessage -> Ctx k -> Constraint
type family IsEmpty msg g where
  IsEmpty msg '[] = ()
  IsEmpty msg g = TypeError msg

-- | The variables of @g@ whose ids are not in @h@.
type Minus :: forall {k}. Ctx k -> Ctx k -> Ctx k
type family Minus g h where
  Minus '[] h = '[]
  Minus g '[] = g
  Minus ('(n, a) ': g) ('(m, b) ': h) = MinusBy (CmpNat n m) ('(n, a) ': g) ('(m, b) ': h)

type MinusBy :: forall {k}. Ordering -> Ctx k -> Ctx k -> Ctx k
type family MinusBy o g h where
  MinusBy GT (x ': g) h = x ': Minus g h
  MinusBy EQ (x ': g) (y ': h) = Minus g h
  MinusBy LT g (y ': h) = Minus g h

-- | The variables of @g@ whose ids are in @h@.
type Inter :: forall {k}. Ctx k -> Ctx k -> Ctx k
type Inter g h = Minus g (Minus g h)

-- $
-- The examples below are compiled at @k = 'Data.Kind.Type'@, where the result can be run.

-- | Swap a tensor.
--
-- >>> import Prelude (Bool (..))
-- >>> swapT @Bool @Bool (True, False)
-- (False,True)
swapT :: forall {k} (a :: k) b. (SymMonoidal k, Ob a, Ob b) => a ** b ~> b ** a
swapT :: forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swapT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a :** F b) \(Term 3 '[ '(1, F a)] (F a)
a, Term 3 '[ '(2, F b)] (F b)
b) -> Term 3 '[ '(2, F b)] (F b)
b Term 3 '[ '(2, F b)] (F b)
%1 -> Term 3 '[ '(1, F a)] (F a)
%1 -> Term 3 (Union '[ '(2, F b)] '[ '(1, F a)]) (F b :** F a)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 3 '[ '(1, F a)] (F a)
a

-- | Apply a function to an argument, both in a tensor.
--
-- >>> import Prelude (Bool (..), not)
-- >>> applyT @Bool @Bool (not, True)
-- False
applyT :: forall {k} (a :: k) b. (Closed k, SymMonoidal k, Ob a, Ob b) => (a ~~> b) ** a ~> b
applyT :: forall {k} (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
applyT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @((F a :-> F b) :** F a) (\Term 1 '[ '(0, (F a :-> F b) :** F a)] ((F a :-> F b) :** F a)
p -> Term 1 '[ '(0, (F a :-> F b) :** F a)] ((F a :-> F b) :** F a)
%1 -> (Term (1 + 2) '[ '(1, F a :-> F b)] (F a :-> F b)
       %1 -> Term (1 + 2) '[ '(1 + 1, F a)] (F a)
       %1 -> Term (1 + 2) '[ '(1 + 1, F a), '(1, F a :-> F b)] (F b))
%1 -> Term 1 (Union '[] '[ '(0, (F a :-> F b) :** F a)]) (F b)
forall {k} (d :: Nat) (g :: Ctx k) (r :: Ctx k) (a :: SYN k)
       (b :: SYN k) (c :: SYN k) (da :: Nat) (db :: Nat).
(Monoidal k, KnownObj a, KnownObj b, Merge r g) =>
Term d g (a :** b)
%1 -> (Term da '[ '(d, a)] a
       %1 -> Term db '[ '(d + 1, b)] b
       %1 -> Term (d + 2) ('(d + 1, b) : '(d, a) : r) c)
%1 -> Term d (Union r g) c
split Term 1 '[ '(0, (F a :-> F b) :** F a)] ((F a :-> F b) :** F a)
p (\Term (1 + 2) '[ '(1, F a :-> F b)] (F a :-> F b)
f Term (1 + 2) '[ '(1 + 1, F a)] (F a)
x -> Term (1 + 2) '[ '(1, F a :-> F b)] (F a :-> F b)
f Term (1 + 2) '[ '(1, F a :-> F b)] (F a :-> F b)
%1 -> Term (1 + 2) '[ '(1 + 1, F a)] (F a)
%1 -> Term
        (1 + 2) (Union '[ '(1, F a :-> F b)] '[ '(1 + 1, F a)]) (F b)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Closed k, KnownObj a, KnownObj b, Merge g1 g2) =>
Term d g1 (a :-> b) %1 -> Term d g2 a %1 -> Term d (Union g1 g2) b
! Term (1 + 2) '[ '(1 + 1, F a)] (F a)
x))

-- | Curry the tensor.
--
-- >>> import Prelude (Bool (..))
-- >>> curryT @Bool @Bool True False
-- (True,False)
curryT :: forall {k} (a :: k) b. (Closed k, SymMonoidal k, Ob a, Ob b) => a ~> b ~~> a ** b
curryT :: forall {k} (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob a, Ob b) =>
a ~> (b ~~> (a ** b))
curryT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a) @(F b :-> F a :** F b) (\Term 2 '[ '(0, F a)] (F a)
x -> (Term 2 '[ '(1, F b)] (F b)
 %1 -> Term 2 (Union '[ '(0, F a)] '[ '(1, F b)]) (F a :** F b))
%1 -> Term 1 '[ '(0, F a)] (F b :-> (F a :** F b))
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
(Closed k, Binds t d a cont r b) =>
(t %1 -> cont) %1 -> Term d r (a :-> b)
lam (\Term 2 '[ '(1, F b)] (F b)
y -> Term 2 '[ '(0, F a)] (F a)
x Term 2 '[ '(0, F a)] (F a)
%1 -> Term 2 '[ '(1, F b)] (F b)
%1 -> Term 2 (Union '[ '(0, F a)] '[ '(1, F b)]) (F a :** F b)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 2 '[ '(1, F b)] (F b)
y))

-- | Rotate a triple, with a triple pattern.
--
-- >>> import Prelude (Bool (..), Int)
-- >>> rotT @Int @Bool @Int ((1, True), 2)
-- ((True,2),1)
rotT :: forall {k} (a :: k) b c. (SymMonoidal k, Ob a, Ob b, Ob c) => a ** b ** c ~> b ** c ** a
rotT :: forall {k} (a :: k) (b :: k) (c :: k).
(SymMonoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> ((b ** c) ** a)
rotT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a :** F b :** F c) \(Term 5 '[ '(3, F a)] (F a)
a, Term 5 '[ '(4, F b)] (F b)
b, Term 5 '[ '(2, F c)] (F c)
c) -> Term 5 '[ '(4, F b)] (F b)
b Term 5 '[ '(4, F b)] (F b)
%1 -> Term 5 '[ '(2, F c)] (F c)
%1 -> Term 5 (Union '[ '(4, F b)] '[ '(2, F c)]) (F b :** F c)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 5 '[ '(2, F c)] (F c)
c Term 5 (Union '[ '(4, F b)] '[ '(2, F c)]) (F b :** F c)
%1 -> Term 5 '[ '(3, F a)] (F a)
%1 -> Term
        5
        (Union (Union '[ '(4, F b)] '[ '(2, F c)]) '[ '(3, F a)])
        ((F b :** F c) :** F a)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 5 '[ '(3, F a)] (F a)
a

-- | Trace out @u@ with a @rec@ block. In 'Data.Kind.Type' the trace is a lazy fixed point.
--
-- >>> import Prelude (Int, take)
-- >>> traceT @Int @[Int] @[Int] (\(a, u) -> (take 3 u, a : u)) 1
-- [1,1,1]
traceT :: forall {k} (a :: k) b u. (TracedMonoidal k, Ob a, Ob b, Ob u) => (a ** u ~> b ** u) -> a ~> b
traceT :: forall {k} (a :: k) (b :: k) (u :: k).
(TracedMonoidal k, Ob a, Ob b, Ob u) =>
((a ** u) ~> (b ** u)) -> a ~> b
traceT (a ** u) ~> (b ** u)
h = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a) \Term 1 '[ '(0, F a)] (F a)
a -> Proarrow.Tools.SMC.do
  rec (b, u) <- lift @(F a :** F u) @(F b :** F u) h (a * u)
  b

-- | Trace out @u@ with 'loop'.
--
-- >>> import Prelude (Int, take)
-- >>> loopT @Int @[Int] @[Int] (\(a, u) -> (take 3 u, a : u)) 1
-- [1,1,1]
loopT :: forall {k} (a :: k) b u. (TracedMonoidal k, Ob a, Ob b, Ob u) => (a ** u ~> b ** u) -> a ~> b
loopT :: forall {k} (a :: k) (b :: k) (u :: k).
(TracedMonoidal k, Ob a, Ob b, Ob u) =>
((a ** u) ~> (b ** u)) -> a ~> b
loopT (a ** u) ~> (b ** u)
h = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a) \Term 2 '[ '(0, F a)] (F a)
a -> forall {k} (u :: SYN k) (b :: SYN k) (d :: Nat) (r :: Ctx k) t
       cont.
(TracedMonoidal k, KnownObj b, Binds t d u cont r (b :** u)) =>
(t %1 -> cont) %1 -> Term d r b
forall (u :: SYN k) (b :: SYN k) (d :: Nat) (r :: Ctx k) t cont.
(TracedMonoidal k, KnownObj b, Binds t d u cont r (b :** u)) =>
(t %1 -> cont) %1 -> Term d r b
loop @(F u) \Term 2 '[ '(1, F u)] (F u)
u -> forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(F a :** F u) @(F b :** F u) (a ** u) ~> (b ** u)
Interp (F a :** F u) ~> Interp (F b :** F u)
h (Term 2 '[ '(0, F a)] (F a)
a Term 2 '[ '(0, F a)] (F a)
%1 -> Term 2 '[ '(1, F u)] (F u)
%1 -> Term 2 (Union '[ '(0, F a)] '[ '(1, F u)]) (F a :** F u)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 2 '[ '(1, F u)] (F u)
u)

-- | A trace from the duality alone, so for any compact closed category: feed @u@ in along one
-- end of a new pair and join its new value with the other end.
loopCC :: forall {k} (a :: k) b u. (CompactClosed k, Ob a, Ob b, Ob u) => (a ** u ~> b ** u) -> a ~> b
loopCC :: forall {k} (a :: k) (b :: k) (u :: k).
(CompactClosed k, Ob a, Ob b, Ob u) =>
((a ** u) ~> (b ** u)) -> a ~> b
loopCC (a ** u) ~> (b ** u)
h = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a) \Term 3 '[ '(0, F a)] (F a)
a -> Proarrow.Tools.SMC.do
  (u, u') <- Term 1 '[] (F u :** D (F u))
forall {k} (a :: SYN k) (d :: Nat).
(CompactClosed k, KnownObj a) =>
Term d '[] (a :** D a)
produce
  (b, v) <- lift @(F a :** F u) @(F b :** F u) h (a * u)
  () <- annihilate u' v
  b

-- | A snake: create a pair, join its dual with the input, and continue with the other end. By the
-- zigzag law it is the identity. The input is older than the pair, so it sits to the left of it,
-- and the join needs a swap.
snakeT :: forall {k} (a :: k). (CompactClosed k, Ob a) => a ~> a
snakeT :: forall {k} (a :: k). (CompactClosed k, Ob a) => a ~> a
snakeT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a) \Term 3 '[ '(0, F a)] (F a)
x -> Proarrow.Tools.SMC.do
  (a, a') <- Term 1 '[] (F a :** D (F a))
forall {k} (a :: SYN k) (d :: Nat).
(CompactClosed k, KnownObj a) =>
Term d '[] (a :** D a)
produce
  () <- annihilate a' x
  a

-- | The inverse of 'distribDual': make a pair for @a ** b@, and annihilate the two halves of its
-- plain end with the given duals.
combineDualT :: forall {k} (a :: k) b. (CompactClosed k, Ob a, Ob b) => Dual a ** Dual b ~> Dual (a ** b)
combineDualT :: forall {k} (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
(Dual a ** Dual b) ~> Dual (a ** b)
combineDualT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(D (F a) :** D (F b)) @(D (F a :** F b)) \(Consumer 7 '[ '(1, D (F a))] (F a)
da, Consumer 7 '[ '(2, D (F b))] (F b)
db) -> Proarrow.Tools.SMC.do
  (ab, ab') <- Term 3 '[] ((F a :** F b) :** D (F a :** F b))
forall {k} (a :: SYN k) (d :: Nat).
(CompactClosed k, KnownObj a) =>
Term d '[] (a :** D a)
produce
  (a, b) <- ab
  () <- annihilate da a
  () <- annihilate db b
  ab'

-- | The tensor distributes over the coproduct: the shared @a@ goes to whichever branch is taken.
--
-- >>> import Prelude (Bool (..), Char, Either (..), Int)
-- >>> distT @Int @Bool @Char (1, Left True)
-- Left (1,True)
distT
  :: forall {k} (a :: k) b c. (Distributive k, SymMonoidal k, Ob a, Ob b, Ob c) => a ** (b || c) ~> (a ** b) || (a ** c)
distT :: forall {k} (a :: k) (b :: k) (c :: k).
(Distributive k, SymMonoidal k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a :** (F b :|| F c)) \(Term 3 '[ '(1, F a)] (F a)
a, Term 3 '[ '(2, F b :|| F c)] (F b :|| F c)
bc) ->
  Term 3 '[ '(1, F a)] (F a)
%1 -> Term 3 '[ '(2, F b :|| F c)] (F b :|| F c)
%1 -> ((Term 3 '[ '(1, F a)] (F a), Term 3 '[ '(2, F b)] (F b))
       %1 -> Term
               3
               (Union '[ '(1, F a)] '[ '(2, F b)])
               ((F a :** F b) :|| (F a :** F c)))
-> ((Term 3 '[ '(1, F a)] (F a), Term 3 '[ '(2, F c)] (F c))
    %1 -> Term
            3
            (Union '[ '(1, F a)] '[ '(2, F c)])
            ((F a :** F b) :|| (F a :** F c)))
-> Term
     3
     (Union '[ '(1, F a)] '[ '(2, F b :|| F c)])
     ((F a :** F b) :|| (F a :** F c))
forall {k} (s :: SYN k) (a :: SYN k) (b :: SYN k) (c :: SYN k)
       (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) t1 cont1 t2 cont2.
(Distributive k, KnownObj s, KnownObj a, KnownObj b, Merge g1 g2,
 Binds t1 0 (s :** a) cont1 '[] c,
 Binds t2 0 (s :** b) cont2 '[] c) =>
Term d g1 s
%1 -> Term d g2 (a :|| b)
%1 -> (t1 %1 -> cont1)
-> (t2 %1 -> cont2)
-> Term d (Union g1 g2) c
caseOf Term 3 '[ '(1, F a)] (F a)
a Term 3 '[ '(2, F b :|| F c)] (F b :|| F c)
bc (\(Term 3 '[ '(1, F a)] (F a)
a', Term 3 '[ '(2, F b)] (F b)
b) -> Term 3 (Union '[ '(1, F a)] '[ '(2, F b)]) (F a :** F b)
%1 -> Term
        3
        (Union '[ '(1, F a)] '[ '(2, F b)])
        ((F a :** F b) :|| (F a :** F c))
forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
(HasBinaryCoproducts k, KnownObj a, KnownObj b) =>
Term d g a %1 -> Term d g (a :|| b)
inl (Term 3 '[ '(1, F a)] (F a)
a' Term 3 '[ '(1, F a)] (F a)
%1 -> Term 3 '[ '(2, F b)] (F b)
%1 -> Term 3 (Union '[ '(1, F a)] '[ '(2, F b)]) (F a :** F b)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 3 '[ '(2, F b)] (F b)
b)) (\(Term 3 '[ '(1, F a)] (F a)
a', Term 3 '[ '(2, F c)] (F c)
c) -> Term 3 (Union '[ '(1, F a)] '[ '(2, F c)]) (F a :** F c)
%1 -> Term
        3
        (Union '[ '(1, F a)] '[ '(2, F c)])
        ((F a :** F b) :|| (F a :** F c))
forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
(HasBinaryCoproducts k, KnownObj a, KnownObj b) =>
Term d g b %1 -> Term d g (a :|| b)
inr (Term 3 '[ '(1, F a)] (F a)
a' Term 3 '[ '(1, F a)] (F a)
%1 -> Term 3 '[ '(2, F c)] (F c)
%1 -> Term 3 (Union '[ '(1, F a)] '[ '(2, F c)]) (F a :** F c)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 3 '[ '(2, F c)] (F c)
c))

-- | Swap a coproduct, with nothing to share.
--
-- >>> import Prelude (Bool (..), Either (..), Int)
-- >>> swapEitherT @Int @Bool (Left 1)
-- Right 1
swapEitherT :: forall {k} (a :: k) b. (Distributive k, SymMonoidal k, Ob a, Ob b) => a || b ~> b || a
swapEitherT :: forall {k} (a :: k) (b :: k).
(Distributive k, SymMonoidal k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapEitherT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a :|| F b) \Term 1 '[ '(0, F a :|| F b)] (F a :|| F b)
x ->
  Term 1 '[] I
%1 -> Term 1 '[ '(0, F a :|| F b)] (F a :|| F b)
%1 -> (((), Term 3 '[ '(2, F a)] (F a))
       %1 -> Term 3 '[ '(2, F a)] (F b :|| F a))
-> (((), Term 3 '[ '(2, F b)] (F b))
    %1 -> Term 3 '[ '(2, F b)] (F b :|| F a))
-> Term 1 (Union '[] '[ '(0, F a :|| F b)]) (F b :|| F a)
forall {k} (s :: SYN k) (a :: SYN k) (b :: SYN k) (c :: SYN k)
       (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) t1 cont1 t2 cont2.
(Distributive k, KnownObj s, KnownObj a, KnownObj b, Merge g1 g2,
 Binds t1 0 (s :** a) cont1 '[] c,
 Binds t2 0 (s :** b) cont2 '[] c) =>
Term d g1 s
%1 -> Term d g2 (a :|| b)
%1 -> (t1 %1 -> cont1)
-> (t2 %1 -> cont2)
-> Term d (Union g1 g2) c
caseOf Term 1 '[] I
forall {k} (d :: Nat). Monoidal k => Term d '[] I
unit Term 1 '[ '(0, F a :|| F b)] (F a :|| F b)
x (\((), Term 3 '[ '(2, F a)] (F a)
a) -> Term 3 '[ '(2, F a)] (F a) %1 -> Term 3 '[ '(2, F a)] (F b :|| F a)
forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
(HasBinaryCoproducts k, KnownObj a, KnownObj b) =>
Term d g b %1 -> Term d g (a :|| b)
inr Term 3 '[ '(2, F a)] (F a)
a) (\((), Term 3 '[ '(2, F b)] (F b)
b) -> Term 3 '[ '(2, F b)] (F b) %1 -> Term 3 '[ '(2, F b)] (F b :|| F a)
forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
(HasBinaryCoproducts k, KnownObj a, KnownObj b) =>
Term d g a %1 -> Term d g (a :|| b)
inl Term 3 '[ '(2, F b)] (F b)
b)

-- | A pair both as it is and swapped: each alternative takes the same pair apart in its own way.
--
-- >>> import Prelude (Bool (..), Int)
-- >>> bothWaysT @Int @Bool (1, True)
-- ((1,True),(True,1))
bothWaysT
  :: forall {k} (a :: k) b. (SymMonoidal k, HasBinaryProducts k, Ob a, Ob b) => a ** b ~> (a ** b) && (b ** a)
bothWaysT :: forall {k} (a :: k) (b :: k).
(SymMonoidal k, HasBinaryProducts k, Ob a, Ob b) =>
(a ** b) ~> ((a ** b) && (b ** a))
bothWaysT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a :** F b) \Term 1 '[ '(0, F a :** F b)] (F a :** F b)
p -> (Term 1 '[ '(0, F a :** F b)] (F a :** F b)
 %1 -> Term 1 '[ '(0, F a :** F b)] (F a :** F b))
-> ((Term 3 '[ '(1, F a)] (F a), Term 3 '[ '(2, F b)] (F b))
    %1 -> Term 3 (Union '[ '(2, F b)] '[ '(1, F a)]) (F b :** F a))
-> Term 1 '[ '(0, F a :** F b)] (F a :** F b)
%1 -> Term
        1 '[ '(0, F a :** F b)] ((F a :** F b) :&& (F b :** F a))
forall {k} (s :: SYN k) (a :: SYN k) (b :: SYN k) (d :: Nat)
       (g :: Ctx k) t1 cont1 t2 cont2.
(Monoidal k, HasBinaryProducts k, Binds t1 0 s cont1 '[] a,
 Binds t2 0 s cont2 '[] b) =>
(t1 %1 -> cont1)
-> (t2 %1 -> cont2) -> Term d g s %1 -> Term d g (a :&& b)
with (\Term 1 '[ '(0, F a :** F b)] (F a :** F b)
q -> Term 1 '[ '(0, F a :** F b)] (F a :** F b)
q) (\(Term 3 '[ '(1, F a)] (F a)
x, Term 3 '[ '(2, F b)] (F b)
y) -> Term 3 '[ '(2, F b)] (F b)
y Term 3 '[ '(2, F b)] (F b)
%1 -> Term 3 '[ '(1, F a)] (F a)
%1 -> Term 3 (Union '[ '(2, F b)] '[ '(1, F a)]) (F b :** F a)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 3 '[ '(1, F a)] (F a)
x) Term 1 '[ '(0, F a :** F b)] (F a :** F b)
p

-- | Double negation introduction: a consumer of a consumer of @a@ hands it the @a@.
dniT :: forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
dniT :: forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
dniT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a) @(D (D (F a))) \Term 2 '[ '(0, F a)] (F a)
x -> (Consumer 2 '[ '(1, D (F a))] (F a)
 %1 -> Command 2 (Union '[ '(1, D (F a))] '[ '(0, F a)]))
%1 -> Consumer 1 '[ '(0, F a)] (D (F a))
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) t cont.
(StarAutonomous k, Binds t d a cont r (D I)) =>
(t %1 -> cont) %1 -> Consumer d r a
accept (Consumer 2 '[ '(1, D (F a))] (F a)
%1 -> Term 2 '[ '(0, F a)] (F a)
%1 -> Command 2 (Union '[ '(1, D (F a))] '[ '(0, F a)])
forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
`cut` Term 2 '[ '(0, F a)] (F a)
x)

-- | Double negation elimination, the classical direction: emit an @a@ by giving its consumer to
-- the input.
dneT :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
dneT :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
dneT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(D (D (F a))) @(F a) \Consumer (1 + 1) '[ '(0, D (D (F a)))] (D (F a))
nn -> (Consumer (1 + 1) '[ '(1, D (F a))] (F a)
 %1 -> Command (1 + 1) '[ '(1, D (F a)), '(0, D (D (F a)))])
%1 -> Term 1 '[ '(0, D (D (F a)))] (F a)
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (da :: Nat).
(StarAutonomous k, KnownObj a, KnownCtx r) =>
(Consumer da '[ '(d, D a)] a %1 -> Command (d + 1) ('(d, D a) : r))
%1 -> Term d r a
emit \Consumer (1 + 1) '[ '(1, D (F a))] (F a)
k -> Consumer (1 + 1) '[ '(0, D (D (F a)))] (D (F a))
%1 -> Consumer (1 + 1) '[ '(1, D (F a))] (F a)
%1 -> Command
        (1 + 1) (Union '[ '(0, D (D (F a)))] '[ '(1, D (F a))])
forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
cut Consumer (1 + 1) '[ '(0, D (D (F a)))] (D (F a))
nn Consumer (1 + 1) '[ '(1, D (F a))] (F a)
k

-- | Contraposition: a consumer of @b@ consumes @a@ through @f@.
contraT :: forall {k} (a :: k) b. (StarAutonomous k, Ob a, Ob b) => (a ~> b) -> Dual b ~> Dual a
contraT :: forall {k} (a :: k) (b :: k).
(StarAutonomous k, Ob a, Ob b) =>
(a ~> b) -> Dual b ~> Dual a
contraT a ~> b
f = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(D (F b)) @(D (F a)) \Consumer 2 '[ '(0, D (F b))] (F b)
nb -> (Term 2 '[ '(1, F a)] (F a)
 %1 -> Command 2 (Union '[ '(0, D (F b))] '[ '(1, F a)]))
%1 -> Consumer 1 '[ '(0, D (F b))] (F a)
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) t cont.
(StarAutonomous k, Binds t d a cont r (D I)) =>
(t %1 -> cont) %1 -> Consumer d r a
accept \Term 2 '[ '(1, F a)] (F a)
x -> Consumer 2 '[ '(0, D (F b))] (F b)
%1 -> Term 2 '[ '(1, F a)] (F b)
%1 -> Command 2 (Union '[ '(0, D (F b))] '[ '(1, F a)])
forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
cut Consumer 2 '[ '(0, D (F b))] (F b)
nb (forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k).
CategoryOf k =>
(Interp a ~> Interp b) -> Term d g a %1 -> Term d g b
lift @(F a) @(F b) a ~> b
Interp (F a) ~> Interp (F b)
f Term 2 '[ '(1, F a)] (F a)
x)

-- | Par is symmetric: emit both outputs and hand them to the input the other way round. This is
-- 'Proarrow.Category.Monoidal.StarAutonomous.parSwap'.
parSwapT :: forall {k} (a :: k) b. (StarAutonomous k, Ob a, Ob b) => Par a b ~> Par b a
parSwapT :: forall {k} (a :: k) (b :: k).
(StarAutonomous k, Ob a, Ob b) =>
Par a b ~> Par b a
parSwapT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a :## F b) @(F b :## F a) \Consumer (1 + 2) '[ '(0, F a :## F b)] (D (F a) :** D (F b))
p -> (Consumer (1 + 2) '[ '(1, D (F b))] (F b)
 %1 -> Consumer (1 + 2) '[ '(1 + 1, D (F a))] (F a)
 %1 -> Command
         (1 + 2) '[ '(1 + 1, D (F a)), '(1, D (F b)), '(0, F a :## F b)])
%1 -> Term 1 '[ '(0, F a :## F b)] (F b :## F a)
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k)
       (da :: Nat) (db :: Nat).
(StarAutonomous k, KnownObj a, KnownObj b, KnownCtx r) =>
(Consumer da '[ '(d, D a)] a
 %1 -> Consumer db '[ '(d + 1, D b)] b
 %1 -> Command (d + 2) ('(d + 1, D b) : '(d, D a) : r))
%1 -> Term d r (a :## b)
par \Consumer (1 + 2) '[ '(1, D (F b))] (F b)
kb Consumer (1 + 2) '[ '(1 + 1, D (F a))] (F a)
ka -> Consumer (1 + 2) '[ '(0, F a :## F b)] (D (F a) :** D (F b))
%1 -> Term
        (1 + 2)
        (Union '[ '(1 + 1, D (F a))] '[ '(1, D (F b))])
        (D (F a) :** D (F b))
%1 -> Command
        (1 + 2)
        (Union
           '[ '(0, F a :## F b)]
           (Union '[ '(1 + 1, D (F a))] '[ '(1, D (F b))]))
forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
cut Consumer (1 + 2) '[ '(0, F a :## F b)] (D (F a) :** D (F b))
p (Consumer (1 + 2) '[ '(1 + 1, D (F a))] (F a)
ka Consumer (1 + 2) '[ '(1 + 1, D (F a))] (F a)
%1 -> Consumer (1 + 2) '[ '(1, D (F b))] (F b)
%1 -> Term
        (1 + 2)
        (Union '[ '(1 + 1, D (F a))] '[ '(1, D (F b))])
        (D (F a) :** D (F b))
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Consumer (1 + 2) '[ '(1, D (F b))] (F b)
kb)

-- | Linear (weak) distributivity, @a ⊗ (b ⅋ c) ⊸ (a ⊗ b) ⅋ c@: the @b@ the input emits is paired
-- with @a@ and sent to the first output, and its @c@ goes to the second. This is
-- 'Proarrow.Category.Monoidal.StarAutonomous.weakDistL'.
weakDistT
  :: forall {k} (a :: k) b c
   . (StarAutonomous k, Ob a, Ob b, Ob c)
  => a ** Par b c ~> Par (a ** b) c
weakDistT :: forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
(a ** Par b c) ~> Par (a ** b) c
weakDistT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(F a :** (F b :## F c)) @((F a :** F b) :## F c) \(Term 6 '[ '(1, F a)] (F a)
a, Consumer (3 + 2) '[ '(2, F b :## F c)] (D (F b) :** D (F c))
bc) ->
  (Consumer 6 '[ '(3, D (F a :** F b))] (F a :** F b)
 %1 -> Consumer (3 + 2) '[ '(3 + 1, D (F c))] (F c)
 %1 -> Command
         (3 + 2)
         '[ '(3 + 1, D (F c)), '(3, D (F a :** F b)), '(2, F b :## F c),
            '(1, F a)])
%1 -> Term
        3 '[ '(2, F b :## F c), '(1, F a)] ((F a :** F b) :## F c)
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k)
       (da :: Nat) (db :: Nat).
(StarAutonomous k, KnownObj a, KnownObj b, KnownCtx r) =>
(Consumer da '[ '(d, D a)] a
 %1 -> Consumer db '[ '(d + 1, D b)] b
 %1 -> Command (d + 2) ('(d + 1, D b) : '(d, D a) : r))
%1 -> Term d r (a :## b)
par \Consumer 6 '[ '(3, D (F a :** F b))] (F a :** F b)
kab Consumer (3 + 2) '[ '(3 + 1, D (F c))] (F c)
kc -> Consumer (3 + 2) '[ '(2, F b :## F c)] (D (F b) :** D (F c))
%1 -> Term
        (3 + 2)
        (Union '[ '(3, D (F a :** F b)), '(1, F a)] '[ '(3 + 1, D (F c))])
        (D (F b) :** D (F c))
%1 -> Command
        (3 + 2)
        (Union
           '[ '(2, F b :## F c)]
           (Union '[ '(3, D (F a :** F b)), '(1, F a)] '[ '(3 + 1, D (F c))]))
forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
cut Consumer (3 + 2) '[ '(2, F b :## F c)] (D (F b) :** D (F c))
bc ((Term 6 '[ '(5, F b)] (F b)
 %1 -> Command
         6
         (Union
            '[ '(3, D (F a :** F b))] (Union '[ '(1, F a)] '[ '(5, F b)])))
%1 -> Consumer (3 + 2) '[ '(3, D (F a :** F b)), '(1, F a)] (F b)
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) t cont.
(StarAutonomous k, Binds t d a cont r (D I)) =>
(t %1 -> cont) %1 -> Consumer d r a
accept (\Term 6 '[ '(5, F b)] (F b)
b -> Consumer 6 '[ '(3, D (F a :** F b))] (F a :** F b)
%1 -> Term 6 (Union '[ '(1, F a)] '[ '(5, F b)]) (F a :** F b)
%1 -> Command
        6
        (Union
           '[ '(3, D (F a :** F b))] (Union '[ '(1, F a)] '[ '(5, F b)]))
forall {k} (a :: SYN k) (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k).
(StarAutonomous k, KnownObj a, Merge g1 g2) =>
Consumer d g1 a %1 -> Term d g2 a %1 -> Command d (Union g1 g2)
cut Consumer 6 '[ '(3, D (F a :** F b))] (F a :** F b)
kab (Term 6 '[ '(1, F a)] (F a)
a Term 6 '[ '(1, F a)] (F a)
%1 -> Term 6 '[ '(5, F b)] (F b)
%1 -> Term 6 (Union '[ '(1, F a)] '[ '(5, F b)]) (F a :** F b)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Term 6 '[ '(5, F b)] (F b)
b)) Consumer (3 + 2) '[ '(3, D (F a :** F b)), '(1, F a)] (F b)
%1 -> Consumer (3 + 2) '[ '(3 + 1, D (F c))] (F c)
%1 -> Term
        (3 + 2)
        (Union '[ '(3, D (F a :** F b)), '(1, F a)] '[ '(3 + 1, D (F c))])
        (D (F b) :** D (F c))
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k).
(Monoidal k, Merge g1 g2) =>
Term d g1 a %1 -> Term d g2 b %1 -> Term d (Union g1 g2) (a :** b)
* Consumer (3 + 2) '[ '(3 + 1, D (F c))] (F c)
kc)

-- | The snake on the dual: join the input with the first end of a new pair, and continue with the
-- second. Here the wires meet in the order they come, so no swap is needed.
snakeDualT :: forall {k} (a :: k). (CompactClosed k, Ob a) => Dual a ~> Dual a
snakeDualT :: forall {k} (a :: k). (CompactClosed k, Ob a) => Dual a ~> Dual a
snakeDualT = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds t 0 a cont '[] b) =>
(t %1 -> cont) -> Interp a ~> Interp b
toSMC @(D (F a)) \Consumer 3 '[ '(0, D (F a))] (F a)
x -> Proarrow.Tools.SMC.do
  (a, a') <- Term 1 '[] (F a :** D (F a))
forall {k} (a :: SYN k) (d :: Nat).
(CompactClosed k, KnownObj a) =>
Term d '[] (a :** D a)
produce
  () <- annihilate x a
  a'