wires

Worth mentioning that we are offering a high-quality (paid) course https://training.statebox.org

you have to understand that the real power behind this work is not the Petri nets but that fact that they are described so abstractly that they can take on different shapes, such as stochastic nets, or coloured nets, or...

It puts the different models on the same footing (and hence allowing you to unify tools and do more work)

Also, I'd even argue that biology/chemistry needs to embrace categorical methods and we would see some deep discoveries.

Not at all. We have been applying category theory for the past few years to software and systems design and this paper in particular came as a result of those implementations.

Soon these methods will be usable by many people for all kinds of purposes. You can think of cryptographic contracts, business process execution, game theory, functional reactive programming, quantum protocols and digital or analogue electronics.

The only difference is what category the diagrams live in, or put another way, which semantics are you assigning to thee boxes and wires.

You can stay tuned on statebox.org and process.io

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.

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

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

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

(co-author of typedefs here): having real ADTs with sum/coproduct type constructors is indeed one of the motivations behind typedefs.

re [1] the language behind ATD seems really similar to typedefs (not surprising, it is the "sane" choice) I need to give it a deeper look to point out more subtle differences. Additionally since we developed in Idris we provide proofs that `serialized . deserialize = id`, which is not possible in OCaml.

regarding [2], it's the same idea, except that doesn't follow any well establish type theory or other mathematical structure as the basis of it's language:

                   Compound = Record
                            | Sequence
                            | Set
                            | Dictionary

There is a payoff between strictness and usability. To be more precise in the type system beyond what typedefs has now, you need to involve more complicated stuff such as dependent types or refinement types. I don't have the answer, but having (co)products and recursion seems like a reasonable starting point.

Exactly. We are talking to some people at NIST about a categorical way to do units, which we hope to add to typedefs. I don't think any of the research around this is published yet

hey thanks for the extensive comments. We were not ready to hit HN per se, our web pages and examples certainly can use some brushing up. André Videla has been doing some nice work on tutorials, but it is hard to find. https://github.com/typedefs/typedefs/blob/master/TUTORIAL_UN...

As for your last question, for this we have been working on "specialization" where you would say Bool is actually Bool in Haskell and not Either Unit Unit etc.

I will try to see if I can address your questions properly as I refresh some copy on the homepage.

Thanks for the comment, this is indeed the vision. We still have a lot of work to do in terms of making the language very user friendly. But theoretically speaking F-Algebra's seem like a good candidate theory for such a language (Typedefs is currently using F-Algebra's, but we started the project thinking about Polynomial Functors as a base theory- and this is still ongoing research).

this is indeed quite nice, but the difference with Typedefs is that we have real ADT's whereas typescript doesn't.

in theory typedefs should be able to do what spot does, it is just very hard to write formalized code so it will take us a while before we get there

so was I :-)

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

hi,

I know Statebox pretty well :)

Luna not super well, but I did beta test their first release (and some later versions), cool stuff.

Anyway, the two are (feature wise) very similar, as you noted:

- both have textual/visual representations, - are typed FP languages, - access to FFI/effects, - diagram nesting

But Statebox is _not_ data-flow, it's more about "control flow" or "multi-party protocol execution". (You could do data-flow with Statebox, but at the moment that's prohibitively inefficient.)

Where Statebox takes a different direction (I think) is in basing the language on established concepts from category theory and focussing on 'generality/compositionality' ; specifically, our diagrams are not "graphs", but (morphisms in) categories.

This difference is very very subtle, in fact, seems totally irrelevant if you want to visual programming (see the nice codex, clearly it works using graphs!)

but it becomes more important when you want to diagram's to be "universal". at least in principle, the Statebox language should naturally and compositionally translate to any kind of hardware ; we want you to be able to program smart contracts, p2p-systems, JS frontends, digital circuits, heck, maybe even slime molds, all from the same diagram.

Luna certainly has more features at this stage.

(also, our editor is under heavy development and not yet published, we are aiming to release some things around the statebox summit in september)

Maybe it's fair to say: Luna is like a better NodeRED, Statebox is conceptually closer to something like homotopy.io / globular.science ?

Hope this clears things up a bit

It's a true community sharing all their music.

That's the point. Sharing is caring. Also this is what culture is about... not about the pop shit we get shoved in our face all the time. If anything, mp3 sharing made me buy more records (12" vinyl), not less.

I wish there was something drastically simpler

Have you tried Nomad?

https://www.nomadproject.io

yep UML and such don't have what we think of as sensible semantics.

if you really do it right, the high-level design might enable you to specify type-like properties that constrain the low-level implementation in a broadly helpful way

so this is exactly what we do. we have a general way to specify boxes and wires and if you give me some sort of type system and a functor and voila, we can produce some well behaved code. nothing is hand-wavy about it, or "complex", like specialized flags or properties of boxes, just some simple mappings

i completely dismiss scratch as an actual visual programming environment.

well put, couldn't agree more, I often use scratch as an anti example of diagrammatic programming.

visual programming has this topological aspect to it (move a box around and don't change the program), and it demands compatibility with this from the underlying thing, whatever it is, state machines or stream processing functions or whatever.

labview is a great example of a practical use of it, which some relatively minor, but critical modifications you can use it for so many more applications... maybe one day statebox can fill that gap, but we have a lot to do still

exactly this.

in general it is harder to build tools for graphical languages, I think this has been prohibitive. parser are hard, but diagrams require constraint solvers and what not, on top of the parsing.

but we came a long way since 1990, both on our actual abilities to build the stuff (JS and the browser can do powerful visual things) but we also understand functional programming and it's relation to mathematics much better.

anyway, thanks for your comments! Nice thread and you are 100% right with the TODO list; we actually build a tool (here is a basic pre-version https://github.com/wires/roadmap-viewer) to manage the intricate roadmap needed for this big project. Stay tuned! :-)

this is exactly where the statebox project comes from, there is updated syntax for mathematics in the form of diagrams. of course not for all of it, but certainly very applicable to CS stuff

very well put!

now you can. ok, well soon :) but the theory is in place and works. Also stochastic Petri nets are actually equivalent to Feynman diagrams in a precise sense (https://johncarlosbaez.wordpress.com/2012/12/20/petri-net-pr...), they could be the Feynman diagrams of functional programming :)

also, ideally the precision in the statebox kernel is hidden from the user.. nobody needs to really know about profunctors or monoidal categories, unless you want to work on the language tooling itself.

anyway, interesting discussion

gnu radio is cool

but these are different problems:

- macros for diagrams, n-bit-adder for any n - "boxing up" diagrams, or some sort of nesting of diagrams - management of state

there are separated concepts in our tool, macros are a 'meta language', in principle one can write functions in the host language that generate diagrams and then proof that those diagrams are well behaved in some way. there is theory on how to do this for diagrams, but we have not implemented any of this yet

boxing up is a natural operation of the system; we get that for free sort of

state is handled by folding functions over the history, so you get a nice and clean way of dealing with state

but you are right, this ability is very important; it is a lot harder to do tho, but it's possible now I think

You are talking about deficits in the tools to work with graphical representations and lack of language support to contain behaviour to a single box (like a decent type system and separation of effects from pure computation)

I am the first person to admit that visual programming goes wrong about 95% of the time, but it doesn't have to... also nobody is expecting everyone to swap out their tools for statebox haha

I also disagree with general applicability :-)

But fair enough, I hear this a lot.

OTOH, a side-effect of working categorically is that we really assume very little, so we can apply the system is many things (at least the core doesn't restrict us, of course you still need to write code etc).

this is unlike all other systems which are domain specific.

you should think of it much more like an alternative syntax for bits of constrained Haskell code... anyway, thnx for the feedback, I am mainly surprised to see this on HN =)

the diagrams are just different ways to draw expressions, you are actually editing text, it's really the same data. one diagram implies many different but behaviourally equivalent expressions, so the diagram is actually the more efficient way to encode the thing

this is ignoring all the UX issues of course. but we are quite confident eventually everyone will use such diagrams as at least sidekicks in their text-based-code

it is in fact very helpful to model out your error states, esp. if you can see it on a screen in some sort of flow. this is why people do modelling, to understand better what you want to code.

But you are right, there are many things that are difficult to express graphically (at the moment) but I think this can be solved in the near future

we are working on the MVP, getting there, this wasn't supposed to blow up yet, don't want to give any wrong impressions.

currently a lot of our efforts are going into a core component of statebox, https://github.com/typedefs it is library similar to protocol buffers, but it fits well with proof assistants / functional languages / category theory

totally what statebox is trying to do, we take some theory to put the diagrams in the right place and take it from there! thanks for mentioning these tools, they are all awesome to use

FWIW, I found that we can develop a "business process" with a client and get very valuable feedback from the domain expert, who might know very little about computers. I don't really see myself live coding with a non technical client