Documentation

Interpret a closed term (no free variables) into an actual morphism of the target category: move the empty context from the terminal object to the monoidal unit, lower the function-valued term (a closed one needs no arguments to uncurry), and fold into k with generators interpreted by unwrapping Id (the free category was built over k's own hom-sets directly).

Bind a variable, HOAS-style: the function argument stands for the newly bound variable, usable (via Cast) in the body of this lam and any lam nested inside it. The body is a morphism out of the context product, but curry wants the tensor, so the Cartesian coercion mediates.

Function application.

Embed a morphism of the target category as a term between embedded objects.

Inject as the left/right branch of a sum.

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

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

The context product: Mul i is the single object standing in for "all the bound variables in i", a right fold with the most-recently-bound variable last. This mirrors Proarrow.Category.Monoidal.Strictified's Fold, which puts its head leftmost. Fold itself can't be reused, since curry/fst/snd expect the thing being abstracted over on the right of the product.

Cast i j holds when context i is context j with zero or more extra variables pushed on top, letting a term built for j be used anywhere "deeper" than j.

The structures of a bicartesian closed category as a list for FREE: the five BiCCC classes, the Cartesian marker supplying the formal tensor = product coercions (the free category cannot state that type equality itself), and Distributive, for case analysis in the presence of a context.

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

Inject as the right element of a sum.

>>> import Prelude (Bool (..))
>>> injectRight @Bool @Bool True
Right True

Swap a product.

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

Apply a function to an argument, both bundled in a product.

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

Curry a pairing function.

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

Flip the argument order of a 3-argument curried function, applying the last argument twice. This exercises three levels of nested lam and Cast weakening across all of them.

>>> import Prelude (Bool (..))
>>> flipCurried3 @Bool @Bool @Bool (\_ a _ -> a) True False
True

Swap a sum, via either.

>>> import Prelude (Bool (..), Either (..))
>>> swapSum @Bool @Bool (Left True)
Right True
>>> swapSum @Bool @Bool (Right False)
Left False

Eliminate a sum by applying whichever of the two functions matches the branch actually present.

>>> import Prelude (Bool (..), Either (..), not)
>>> caseEither @Bool @Bool @Bool (Left True, (not, id))
False
>>> caseEither @Bool @Bool @Bool (Right True, (not, id))
True