Span Graph via the State Construction

This is a library of open transition systems. The library allows us to declare a morphism in Span(Graph) as a string diagram (using a dedicated DSL for Haskell) and compile it to a transition system.

For instance, the following code,

norLatch :: Spans '[Bool,Bool] '[Bool,Bool]
norLatch =
  ((>)) wire |*| codiscard |*| codiscard |*| wire
   |>|  wire |*|   copy    |*|   copy    |*| wire
   |>|       nor     |*| swap  |*|       nor
   |>|    copy  |*| wire   |*|  wire |*|  copy
   |>|  wire |*| cocopy    |*|   cocopy |*|  wire
   |>|  wire |*| discard   |*|  discard |*|  wire

constructs the NOR latch from its basic components. The resulting transition system can be then depicted using the library to be the following.

Unbiased Arrows

Why? Arrows in Haskell capture theories of processes as premonoidal categories with an identity-on-objects premonoidal functor from Sets (the so-called Freyd categories).

The problem with arrows is that you need to input coherence morphisms by hand. The following is some code I wrote. The real diagram is on the left, but on the right we have a bunch of coherence morhpisms.

ehrenfest = fbk                                 $ runitS>>> lunitinv *** lunitinv
  >>> (full *** idS) *** (empty *** idS)    >>> runitinv
  >>> (fby *** fby) *** unif
  >>> idS *** copy                          >>> associnv >>> idS *** assoc
  >>> idS *** (sigma *** idS)               >>> idS *** associnv >>> assoc
  >>> move *** move
  >>> copy *** copy                          >>> associnv >>> idS *** assoc
  >>> idS *** (sigma *** idS)                >>> idS *** associnv >>> assoc

It would be better if the computer would write these coherence morphisms for us. This is the purpose of this library. Using the library, the following diagram compiles.

diagramSpan :: Spans '[Bool] '[Bool]
diagramSpan =
  ((>))  codiscard  |*|  wire
   |>|      copy    |*|  wire
   |>|   wire  |*|  nor
   |>|   wire  |*|  copy
   |>|      cocopy  |*|  wire
   |>|      discard |*|  wire

Set-based Freyd-categories are just very particular cases of the notion of premonoidal category: conjunctive queries, spans of graphs or vector spaces are examples of premonoidal category. If we want to be able to capture all of these, we need to be able to surpass the restriction saying that Arrows may have the same objects as normal functions. For this, we also introduce Premonoidal as an Arrow possibly constrained on objects.