wires

5 yıl öncediscuss

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

5 yıl öncediscuss

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.

wires

5 yıl öncediscuss

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

wires

6 yıl öncediscuss

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.

wires

6 yıl öncediscuss

(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

This is mathematically already quite complicated.

wires

6 yıl öncediscuss

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.

wires

6 yıl öncediscuss

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

wires

6 yıl öncediscuss

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.

wires

6 yıl öncediscuss

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

wires

6 yıl öncediscuss

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

wires

6 yıl öncediscuss

so was I :-)

wires

6 yıl öncediscuss

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

wires

7 yıl öncediscuss

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

Submissions

Second Order Effects of the Coronavirus

comments