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

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

Preserves has an equational theory. It's untyped, though, like S-expressions, JSON and XML.

Are better examples on the TODO list? I read through the basic examples but felt like it skipped over some things (like the specialized types, and why the examples don't work when compiling to ReasonML). Will I be able to make JSON decoders/serializers of primitive types just like with ATD gen?

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.

by all levels of strictness I don't mean being as strict as possible. I meant it should accommodate for less strict usages as well as strict usages.

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.

No problem! Glad if I can do a little part to help -- It's not that the tutorial / guide that is there is bad, it's just the order! I think a lot of people might try to jump in, since you can basically read protobuf/thrift as-is, but many might not have even heard of GADTs. It might make sense to put just a tiny blurb of an introduction (or even a code sample like bool) on that first page.

I think protobuf's main page[0] is the best example, and thrift's[1] isn't terrible.

Would probably make it easier for lazy developers like me to immediately understand what's going on, and how to be productive.

[0]: https://developers.google.com/protocol-buffers/

[1]: https://thrift.apache.org/

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

Cool! Thanks for the comment. As I said have been a fan of this project (sidenote: love the name and simple, well designed site).

I have played around with a language dubbed WWT (for "World Wide Types") https://jtree.treenotation.org/designer/#standard%20wwt). Instead of starting with the type system and working my way toward the user have gone the other way starting with the "what would the simplest language look like for building types" and worked my way toward the type system (just compiles to TypeScript for now). My thought is it should be editable in Excel.

What I think needs to happen for TypeDefs (or similar) to nail this, is to create a type language that solves the "last mile" problem. Every organization in the world has their own perspective on things, and will need to extend/modify some global CommonTypes repository. So a great type language would be something that worldwide CommonTypes could be defined in, but that is easy for a dev at the local real estate agent's office to write some code and extend. An "HTML for Types" in that sense. Just a guess.

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

> real ADT's

I always thought these examples were real ADT's:

``` type Bool = true | false;

type Maybe<T> = T | null;

type SumTypeExample = Bool | Maybe<Bool>

interface ProductType1 { b: Bool c: Maybe<Bool> }

interface ProductType2 { s: "a" | "b" | "c" }

interface ProductTypeComposite extends ProductType1, ProductType2 {} ```

Can you explain what's the difference?

> we have real ADT's whereas typescript doesn't.

This sounds interesting. Can you expound a bit more?

This is vague and anecdotal but I find about 80% of what I want to do in TS with types I find very easy to do, 10% I find annoying but possible, and then maybe 10% it just doesn't work.

I'm curious if there's a root cause here.

so was I :-)