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.

wires

5 年前議論

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 年前議論

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 年前議論

(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 年前議論

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 年前議論

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 年前議論

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 年前議論

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 年前議論

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 年前議論

so was I :-)

wires

6 年前議論

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

投稿

Second Order Effects of the Coronavirus

コメント