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.

[byorgey]

I have a very rough sketch of a type system on the base-caps branch. But I'm getting kind of sick of it so I'm going to switch to working on something else for a while. Maybe a simpler approach will suggest itself.

[byorgey]

I did a bunch more work on the base-caps branch, but it's still incomplete---I got sick of it again. Need to get back to it at some point. The basic idea is that any type representing some kind of delay (function, delay, or command) carry a capability set annotation, and our basic judgment is now of the form Gamma |- t : sigma ; Delta meaning "In context Gamma, t has type sigma, and its evaluation requires capabilities Delta". We also need capability set polymorphism. See https://github.com/swarm-game/swarm/blob/bef7acb28b2f742cf891a59c9d1997491ecd128a/docs/ott/swarm.pdf .

Checking this involves generating capability set inequalities with both literal capabilities and capability set variables:

(20:33) <   byorgey> Given a set of such subset constraints, we need to find an assignment of a capability set to each variable that satisfies all the constraints, ideally "minimal" capability sets (though I don't imagine the solutions will be unique in general).
(20:34) <   byorgey> In other words we need a solver for... sets of inequalities over a free idempotent commutative monoid?  I think that's the technical way to describe it.
(20:35) <   byorgey> Just wondering if anyone has seen anything like this before.  Though I think it shouldn't be too hard to work out.
(20:39) <   byorgey> I'm imagining some kind of fixed point iteration where we initialize all the variables to the empty set; then on each iteration we look at each inequality and see if there are any capabilities that show up on the LHS but not the RHS.  If so, we add them to the RHS by adding them to one of the 
                     variables on the RHS (and if there aren't any variables on the RHS then signal an error).
(20:40) <   byorgey> But if there are multiple variables on the RHS we have a choice of which one to modify.  I'm not sure how to think about generating a "best" assignment, or what that would even mean, or how much it matters.

[byorgey]

Wanted to update this with my latest thinking on a unified effect system for capabilities/requirements since it has changed quite a bit since the most recent comments above.

• After merging Add require directive #533 we now have "requirements" instead of just a set of capabilities. Requirements consist of:
  • A set of capabilities
  • A multiset of entities required in the inventory
  • A set of devices required to be installed.
• The typing judgment indeed becomes Gamma |- t : sigma ; Delta as mentioned above, meaning "under context Gamma, term t has type sigma and has requirements Delta." Delta are the requirements to evaluate (not execute) term t.
• We don't need any kind of stack, count of levels, etc. Dealing properly with build etc. will be taken care of by the combination of (1) now making a distinction between required capabilities and required inventory, and (2) embedding requirements within types as explained below.
• Any type which represents some sort of "delayed evaluation/execution" also carries a requirement embedded in the type itself. (I have learned that this is a standard technique for effects type systems.) This includes:
  • cmd types carry the requirements to execute the term.
  • A function type carries the requirements to evaluate the function body once the function is applied.
  • A delay type carries the requirements to evaluate the delayed expression.
  • There might be one or two others I'm forgetting at the moment.
• There will be a special typing rule for applications of build. In order to build a robot which needs certain devices installed, you must have those devices in your inventory. So the requirements for build {p} will be derived from the requirements for p by taking the required device set and adding it to the required inventory instead. This will properly deal with nested or multiple calls to build, etc.
• There will certainly need to be an "escape hatch" (Ability to selectively override requirements analysis during build #921) to override the automatic requirements analysis since it will be necessarily conservative.
• For example, we won't be able to do anything very sensible with recursion. If you have a recursive function that calls build, how can we tell how many times build will end up being called, and thus how many copies of the relevant devices we will need? The answer is: we can't. Maybe we can generate a warning in this case.

[xsebek]

If you have a recursive function that calls build, how can we tell how many times build will end up being called, and thus how many copies of the relevant devices we will need?

@byorgey I would argue an infinite amount should suffice 😄

• Infinite items in inventory #621

[byorgey]

I would argue an infinite amount should suffice

Well, yes, an infinite amount would certainly suffice, but that would not be a useful answer, because then it would be impossible to run any recursive functions that call build unless you are in creative mode.

But thinking about it a bit more, perhaps that is indeed the right answer, coupled with some kind of escape mechanism whereby you can say "I know the requirements system cannot prove that this call is safe, but I want to run it anyway". Put another way, given infinite counts, we could design the requirements analysis so that it is always conservative/safe, but recognize that in some cases (especially recursive calls) we will need to provide an escape hatch to allow running things where the analysis is too conservative.

[xsebek]

@byorgey it could also be a challenge or a normal item providing unlimited supply. 🙂

I like the idea of a message saying it calculated an unbounded item requirements. 👍

[byorgey]

it could also be a challenge or a normal item providing unlimited supply.

Yes, that's true, I just meant that in general you cannot count on having an infinite amount of something, e.g. if you write a recursive function while playing the classic game.

[byorgey]

Another example program that ought to work but currently doesn't:

def pr = require 1 "rock"; move; place "rock" end
def x4 = \c. c;c;c;c end
build {turn east; x4 pr}

This ought to build a robot equipped with four rocks. Currently, it is equipped with only one rock, which it places and then crashes when it tries to place the next one.

I know exactly why this happens: when checking the requirements of x4 pr we just check the requirements of x4 and the requirements of pr and then union them, which is not correct of course. We need to infer a type for x4 which is something like forall (a : Type) (r : Reqs). Cmd r a -> Cmd (4r) a. (I have made up this notation, and I'm not suggesting we should show such types to the user by default, but hopefully the basic idea is clear.)

[xsebek]

@byorgey could you please add that as a failing test case? 🙂