5
$\begingroup$

It seems to me that in a statically typed, object oriented language, there is a striking similarity to wiring diagrams. Wires (objects) of type $X$ go into functions (boxes) of input type $X$. Is the corresponding string calculus that of a symmetric monoidal category?

Edit: it has been suggested that I formulate a more specific question. Here goes: let the programming language have private member variables. At this point you cannot copy arbitrary objects because the data is hidden. I guess you also have to assume that there is no generic copy method for all types. Becasue copying isn't allowed arbitrarily, we might need a monoidal category to handle the semantics. Is this the case?

Improve this question
$\endgroup$
1
  • 5
    $\begingroup$ There are various features of programming languages you might want to be capturing and it's unclear to me which ones you intend. The basic one is that type systems can be described as categories where the objects are types (e.g. int or string) and the morphisms are functions with the prescribed input and output types. Then you can go on to ask for more features of the type system (e.g. product types), which corresponds to asking for more from the category (e.g. finite products). See also the Curry-Howard-Lambek correspondence. You should ask a more specific question. $\endgroup$
    – Qiaochu Yuan
    Commented Oct 27, 2015 at 18:39

1 Answer 1

Reset to default
4
$\begingroup$

No full answer but just some random thoughts on the issue:

Concerning the string diagram calculus: It should be that of a mutlicategory (see David Spivaks paper on the Wiring Operad: http://arxiv.org/abs/1305.0297).

Plus I think there's a hidden issue here: Private member variables are only of real concern if the objects are stateful; Otherwise - if they are not observable after object instantiation a.k.a. function call - they can just be considered implementation details. I don't think modelling the wiring between the objects using a multicategory / monoidal category is an approach powerful enough to reason about mutable state. But I guess by adding labels to the diagrams (similar to Petri nets) and let them vary over time this could be fixed. (Again, consult David Spivak for an idea on how to model such a labeling: http://math.mit.edu/~dspivak/informatics/olog.pdf)

EDIT: Concerning the labeling - a rough sketch: A typing of the diagrams at hand shoult propably be used as input to some sort of grothendieck construction and a labeling should then be a lift of the base diagram into the respective fibration. Including Maybe/Option/Exception Types should allow for partial diagrams while the program is still 'booting'.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .