contextual computation limit system in wit language

[dannypsnl]

To extend #150, I'm thinking about an extension that introduce some contextual type system.

1. static reasoning
2. async is a world description
3. own and borrow is a linear restriction

Rules

Here is how it work

• o : T [own]
• b : T [borrow]
• fo : T [own] -> ?
• fb : T [borrow] -> ?
• afo : T [own] -> ? <async>
• afb : T [borrow] -> ? <async>

1. sync world
   1. fb o, fb b: ok
   2. fo o: ok, but later program cannot use o
2. async world
   1. afb o, afb b: ok, but have to wait a signal that shows borrow is complete
   2. afo o: ok, no waiting, but have to ensure this is not in a waiting list

The idea behind these rules is own and borrow is fine to restrict under usual sync programming, but for async program, we will not know when does borrowing complete. Therefore, introduce a special operator to tell the program is waiting for a complete signal can tell a static checker this is fine, program will do the right thing.

For own moving, async world also make us must ensure the moving is unique. The good thing is, since own and borrow are linear restriction, it's easy to find out we are doing it wrong. Therefore, below program is invalid:

foo : T [own] -> unit <async>
foo t = do
  // move & borrow together, wrong
  await [afo t, afb t]

Notice that, we cannot make such program with usual sync world, one must invoke fo first or fb first. But in async programming, some form can do that (like waiting list above).

The t <async> is a monadic t with capabilities limitation, that leads some operators like

1. await : t <async> -> t (bind)
2. return : t -> t <async> (pure)
3. wait_borrow : t <async> -> unit (optional)

As you can see, wait_borrow is not required but maybe an enhancement, since we only need to wait borrowing complete, not the whole computation.

Own/borrow

Let's define a->b means change current status of description, then we have

1. own: 1->0, 1->0
2. borrow: a->a, 1->1 (polymorphic keep first limit)
3. start own: 1, 1
4. start borrow: 0, 1

Therefore

1. fo o changes o : t [1, 1] to o : t [0, 0], and disallow the following use
2. fb o keeps o : t [1, 1]
3. fb b keeps b : t [0, 1]
4. fo b is invalid, since b : t [0, 1] didn't provide [1, 1] for fo

Limitation

For static reasoning, we might have to give up something, like: out of *.wit, disallow ownership description

Conclusion

Hope this is a good start for static reasoning component model programming, I also have some advanced consideration for <> syntax, like <filesystem> can limit the capabilities a program can use. It has two side

1. For runtime, a provider, that's a description about it can access to which thing.
2. For user, that's a restriction, one can only invoke WASI functions under these worlds.