Morphisms as programs

[algebraicjulia]

Morphisms as programs

[epatters]

First, a comment about design. Coincidentally, Mike Shulman has recently published a preprint about a type theory for symmetric monoidal categories. There is a lot going on there, much of which I haven't fully understood, but the discussion in Section 1 is good food for thought.

One relevant issue that Shulman raises is how to deal with monoidal products in the codomain. Suppose you have morphisms f: W -> X x Y and g: X x Y -> Z. How do you write the composite of f with g? Shulman proposes an indexing notation inspired by Sweedler notation, but I think in Julia it will be more natural to write

x, y = f(w)
g(x,y)

(in the spirit of what Shulman calls "covariables") or simply

g(f(w))

Ordinarily, in Julia, only one of these invocations would be allowed. This is the difference between g(x,y) and g((x,y)). For the purpose of parsing Julia programs into morphisms, I think we should allow both. We can do so unambiguously because the morphisms are statically typed. If I understand correctly, Shulman also allows both styles of composition, albeit using the Sweedler notation (see the last two term constructors in Fig 4).

Apart from this subtlety about multiple outputs, and a similar one about nullary outputs (monoidal units), I think we can stick to the ordinary semantics of Julia code.

[epatters]

One way to implement this is to rewrite the Julia program so that:

1. variables carry ports in a wiring diagram
2. function calls create a new box and return its output ports.

The program can then be executed by the Julia run-time and the result will be a wiring diagram.

[epatters]

This issue is now mostly resolved. The only outstanding feature is recovering morphism expressions from traditional expression trees (Formula), but I'll defer that to another issue.