[MaxBarraclough]

Thanks, but you've jumped into detail, where my question was at a more basic level: what's the point? What does this tool do for me? How does it stack up against existing solutions? I've not heard of StateBox.org, for instance, so this doesn't help orient me.

Most programmers don't think in terms of how they've impurely implemented product types. Most programmers don't even know what the term means. For a project like this I think it's important to bring it down to Earth and make it more relatable.

So, somewhat like Protocol Buffers, it's a programming-language-agnostic generator for type-definitions and it also handles language-agnostic serialization. Its unique advantage is that it takes ideas from 'algebraic type' theory to offer strong guarantees when it comes to composing complex types from simpler types. Is that right? edit: on closer reading I don't think it offers serialisation? Worth emphasising this if you compare it against Protocol Buffers.

I also have to agree with pmiller2 that the choice of name is counterproductive. It's hard to google for, and has a misleading C/C++ flavour.

With all that said, it sounds like a neat idea. I like these sorts of 'codified design patterns' that take a code-generative approach and reduce how much code is written by hand. It reminds me of what SCXML does for state machines (although I have no direct experience with that particular solution).

Also, if HN will let you edit, please sort out the italics there.

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