make interchange, currying etc systematic

[JosephNathaniel]

The types associated to our typed lambda expressions often need to be curried, uncurried, interchanged, etc.

The way that these type-juggling operations are currently implemented can be a bit hacky -- e.g. see this instance in our code where we have a try/except block that first tries one thing and then if the types don't work out, tries the interchanged version.

It would be good to figure out how to deal with these type juggling operations systematically. I am unsure if this would be a straightforward adjustment, or if it would require more work.

One tentative idea to deal with interchange is to express it via typed closed lambda terms (combinators).
E.g. if we want to convert a term of type (a->b)x(c->d) to axc->bxd, this can be done by feeding the original term into a combinator (a->b)x(c->d)->(axc->bxd).

[JosephNathaniel]

maybe there is something more conceptual going on here

the interchange operation can be written as a closed lambda term, but to do it in the most general form, would require projection lambda terms, which we have avoided implementing and have been unnecessary thus far

i.e. to be rigorous, a (a->b)x(c->d)->(axc->bxd) combinator would look like λF.λX.((π_1F)(π_1X), (π_2F)(π_2X))

Practically speaking, a main use of interchange happens in n-type expansion, where we have to tensor product two morphisms f : n->n and g : n->n, giving a term of type (n->n)x(n->n), and then interchange this to nxn->nxn so we can plug some nxn argument in.

So for our purposes we could maybe get away with assuming F separates as (f,g), which gets rid of one pair of projections in the combinator.
However, even in this case it will not always hold that X, the thing that gets fed in, separates as (x,y).

[JosephNathaniel]

following on from the previous point: maybe it is possible to avoid the need for interchange after all?
What would actually happen if we feed M : nxn into something like λ(x,y).(fx,gy)?

If this works fine, then at least in the case of n-type expansion, where we want to parallel compose some morphism with identity wires, we can avoid using interchange

e.g. Alice who likes Bob walks:
Avoiding interchange in n-expansion.pdf