[wires]

hi, thanks, that page could surely need an update, I'll see what I can do.

the "problem" with existing systems is that they do not consider their core language with respect to Type Theory nor Category Theory.

Put simply, when I have two type definitions A and B, I would like to be able to construct two new types, (A * B) and (A + B), their product or co-product. You can do this more-or-less in every system, but in typedefs we actually makes sure it is not more-or-less but exactly a product.

This simplifies reasoning about them and embedding the typedefs type theory into something more powerful such as statebox.org

So typedefs provides an implementation of a simple (from the categorical point of view) type system consisting of roughly +, * and recursion \mu.

Statebox adds arrows to this so "A -> B", so things like functions etc. (Really morphisms in monoidal categories, so generalizing funtions and allowing you to work graphically)

Hope this clarifies a bit

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