[wires]

Hm,

our starting point is that there is very good mathematics for expressions like 1 + 2 * 3 which can also be interpreted as a type.

programmers do not know what a product/coproduct is, partly because the existing systems do not properly use that concept.

so what this tool does for you is

  1) decide on a simple theory of types and allows you to define types in this.
  2) implemented that theory in dependent types, so that you can work with typedefs without losing typesafety.

we need this in statebox because we construct diagrams of boxes and typed wires:

      +--+
    A-|f |______ C
    B-|  |
      +--+ +--+
           |g |__ E
    D------|  |
           +--+

here we have two boxes (functions) f : A * B -> C and g: D -> E when we compose (tensor) those as pictures, we get a bigger box [f * g] which has type

  [f * g] : A*B*D -> C*E

In typedefs you can compute this and have compile time guarantees. You cannot do this in protocol buffers (other than at runtime using "dynamic" typing)

so it is really more of a typesystem for finite types (things that can be (de)serialized).

we do have (de)serialization for Idris and Haskell (and working on others). In the Idris version you have a proof that

    serialize . deserialize = id

Either way, we have a while to go before this becomes as user friendly as it should be. We have dane work on a different language frontend that looks more like Haskell which may clear things up a bit.