Morphisms as programs

[epatters]

We want a module for converting morphisms in a symmetric monoidal category to and from programs, by which I mean expressions with variables in the style of type theory. This module will replace what is currently called Catlab.Algebra (#37), and will be called something like Catlab.Programs.

Desired features:

• Morphisms to expression trees, as in conventional CAS
  • Implemented by Formula type
  • See also Community standards for mathematical expression trees #36
• Morphisms from expression trees
  • Not yet implemented
• Morphisms to Julia programs
  • Currently implemented as "algebraic networks"
  • Should be made more general, to support other code generation tasks
• Morphisms (as wiring diagrams) from Julia programs (in subset of Julia language)
  • Not yet implemented
  • See Algebraic Networks <-> Julia Programs #51

I will follow up shortly with ideas about design and implementation.

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