Handle requirements properly as part of the type system

[byorgey]

Describe the bug
It seems that programs run by base are only checked dynamically for capabilities. This means that both

1. The base can get quite a ways through a program before crashing due to a missing capability
2. Some capabilities sneak by since they don't correspond directly to a command and are thus never dynamically checked. For example, recursion is such a capability.

To Reproduce

• Run build "x" {move}; move to see that the base builds the robot "x" first before failing to execute the move due to a missing capability. Ideally, it should instead refuse to run the entire program due to missing capabilities.
• As a different example,

def forever = \c. c ; forever c end
build "x" {forever move}
forever (build "x" {move})

The build "x" fails as it should with an error saying that you don't have the necessarily devices to install on x (namely, a lambda and a strange loop). However, the last line works fine even though it shouldn't, since the base doesn't have a lambda or strange loop.

[xsebek]

Yup, I was wondering if this was intended, but didn't ask, since it makes getting the first lambda harder 😅

[byorgey]

Why does it make getting the first lambda harder?

[xsebek]

It can be hidden behind a lake/mountain and you have to make a program that goes around. ⛰️

Most cases can be solved with "move in one direction, move in other direction and then go back", but that "go back" can be error prone so I used the fetchNW&friends functions. I will just have to write out the first fetch, I guess, no big deal 😉

[byorgey]

So I was trying to work on this today, and ran into what seems like a difficult issue. I put a basic check in place and it immediately started rejecting things like build "x" {move}, because the base does not have treads. Of course this is nonsense: it is x that will be needing treads, not base. But right now capability checking does not treat build specially at all: if it sees an application it simply returns the union of the capabilities required by the left- and right-hand sides of the application.

Clearly, capability checking does need to treat build specially, but I am unsure how to do this in a principled way. We could specially check things which are syntactically arguments to build, but that wouldn't be compositional, i.e. it wouldn't properly deal with custom variants of build. For example, we might define

build2 : string -> {cmd ()} -> cmd ()
build2 name p = build name p; build name p

and now base should be able to execute build2 "x" {move}.

Note higher-order functions make this even trickier. For example, consider a generalization of the above example:

twice : cmd () -> cmd ()
twice c = c ; c

thrice : cmd () -> cmd ()
thrice c = c ; c ; c

buildN : (cmd () -> cmd ()) -> string -> {cmd ()} -> cmd ()
buildN ice name p = ice (build name p)

build2 : string -> {cmd ()} -> cmd ()
build2 = buildN twice

Base should still be able to execute build2 "x" {move} but it now seems harder to figure this out. This example is overly convoluted, of course, but I think it is very realistic to expect that people will write this kind of code.

I'm guessing this means we have to bite the bullet and make capability checking more principled / fine-grained. I will put some thought into what might be required, but happy to hear any ideas and/or pointers to literature (I'm quite sure others have already done similar things).

[byorgey]

Hmm, what if it's as simple as having capability checking return a stack of capability sets instead of a single set? The top of the stack represents capabilities required to evaluate it now. The next thing in the stack represents capabilities needed for things buried inside one level of delay, which would become required after application of force. The next thing down represents capabilities needed for things nested two levels deep, and so on.

• If t requires capability stack S then {t} requires empty : S.
• If t requires capability stack c1 : c2 : S then force t requires c1 ∪ c2 : S.
  In the example, the expression build "x" {move} would end up requiring a stack like 3d printer : treads : empty (I know, those are devices, not capabilities, but you get the idea). Executing it requires only the capabilities in the set on the top of the stack.

I wanted to write this down since it seems interesting, but I am actually not at all convinced that it will allow dealing with higher-order functions.

[byorgey]

More generally, suppose that for each Swarm type tau there is a corresponding (Haskell) type of capability analyses, C(tau).

• For base types B, we have C(B) = [Set Capability]. In other words, for a value of some base type we expect to get a stack of capability sets.
• For a function type tau1 -> tau2, we have C(tau1 -> tau2) = C(tau1) -> C(tau2). In other words, a capability analysis for a function is itself a function which maps capabilities needed for the input to capabilities required for the output. For a given expression we might get a function which ignores or shifts the input (e.g. if the input is ignored or delayed), and/or which unions some extra capabilities (if some are needed to evaluate the function itself).
  • As an example, the capability analysis for build : string -> {cmd ()} -> cmd string should end up being something like \c1 -> \c2 -> [3d print] ∪ c1 ∪ (empty : c2) (where ∪ here denotes something like zipWith union but which extends to the longest of its inputs instead of cutting off at the shortest one like normal zipWith does).

[byorgey]

I have thought about this some more, and I seem to be coming to a few different (interrelated) conclusions.

1. Capabilities should (must?) really be part of types, not a separate analysis done later. i.e. we really have an effect system built into our type system.
   • However, hopefully we can infer all the capability stuff and never make users write it.
2. In addition to the challenge of when capabilities are required for delayed things, partial application is in the mix too. For example, what capabilities are required to evaluate b?

   b : {cmd ()} -> cmd ()
   b = build "x"
   

   I would argue none should be required: a 3D printer should only be required once build is fully applied.
3. Instead of carrying around stacks, it might be enough to annotate each argument type with a natural number indicating the level at which it is used (level n = inside n delays). I am not sure about that yet though.

I am now envisioning something where types can be annotated with a set of capabilities, and function arrows are annotated with levels, or something like that... I'll keep banging away at it.