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.

The object of k a type expression stands for.

Type expressions whose Interp is an object, given that their leaves are.

The identity on the object a type expression stands for.

A term at binding depth d with context g and type a: a morphism from the tensor of the context to 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.

Lift a morphism of the target category to a function on terms.

Copy a term whose type is a comonoid, in Proarrow.Tools.SMC: (x1, x2) <- dup x.

Discard a term whose type is a comonoid, in Proarrow.Tools.SMC: () <- drop x.

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.

Two terms side by side. Their contexts must be disjoint.

Take a tensor apart: the continuation gets a variable for each side and must use both.

The unit, which uses no variables.

Bind a pattern, as for toSMC, whose variables the body must use exactly once. This needs the category to be closed.

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.

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.

Join a dual and its wire into nothing: the counit of the duality, which an isomix category has.

Function application. The function and its argument must have disjoint contexts.

A consumer of a: a term of its dual.

A producer and a consumer meeting: a term of the unit of par.

Par, the dual of the tensor of the duals, interpreted as Par.

A consumer meets a producer: cut k t gives t to k, like applying a continuation. This needs the category to be *-autonomous.

cut with the producer first, as System L writes ⟨t | k⟩: t |> k sends t into k.

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.

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.

Bind two outputs: consumers of a and of b, which the command must use exactly once each, give a producer of their par.

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 of two alternatives on the same input: the product. Each alternative takes the input with a pattern, as for toSMC. This needs products.

The first alternative of a product.

The second alternative of a product.

Use up a term into the unit of the product.

The left injection into a coproduct.

The right injection into a coproduct.

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.

There is no term of Zero, so from one, together with the rest of the context, anything follows.

A context: the variables a term uses, each with its id and type, by descending id.

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.

A context that is known to be empty or not, all the way down.

The identity on the tensor of a context.

The tensor of a context is an object.

The context of two terms used side by side.

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.

A new variable on the right of a context: a unitor if the context was empty, and nothing otherwise.

Two new variables on the right of a context, from their tensor: a unitor if the context was empty, and an associator otherwise.

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.

Bind the right hand side to the pattern of the continuation.

The end of a rec block: all its variables, as the tensor of their context.

Trace a rec block: the variables it uses before binding them are fed back.

GHC's translation of rec refers to fail, but pairs of variables always match.

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.

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.

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.

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.

A rec block after tracing, from its context without the fed back variables to the variables it passes on.

The variables of a rec block, as GHC tuples them up.

Swap a tensor.

>>> import Prelude (Bool (..))
>>> swapT @Bool @Bool (True, False)
(False,True)

Apply a function to an argument, both in a tensor.

>>> import Prelude (Bool (..), not)
>>> applyT @Bool @Bool (not, True)
False

Curry the tensor.

>>> import Prelude (Bool (..))
>>> curryT @Bool @Bool True False
(True,False)

Rotate a triple, with a triple pattern.

>>> import Prelude (Bool (..), Int)
>>> rotT @Int @Bool @Int ((1, True), 2)
((True,2),1)

Trace out u with a rec block. In 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]

Trace out u with loop.

>>> import Prelude (Int, take)
>>> loopT @Int @[Int] @[Int] (\(a, u) -> (take 3 u, a : u)) 1
[1,1,1]

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.

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.

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.

The inverse of distribDual: make a pair for a ** b, and annihilate the two halves of its plain end with the given duals.

Double negation introduction: a consumer of a consumer of a hands it the a.

Double negation elimination, the classical direction: emit an a by giving its consumer to the input.

Contraposition: a consumer of b consumes a through f.

Par is symmetric: emit both outputs and hand them to the input the other way round. This is parSwap.

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 weakDistL.

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)

Swap a coproduct, with nothing to share.

>>> import Prelude (Bool (..), Either (..), Int)
>>> swapEitherT @Int @Bool (Left 1)
Right 1

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