Open byorgey opened 2 years ago
Yup, I was wondering if this was intended, but didn't ask, since it makes getting the first lambda harder :sweat_smile:
Why does it make getting the first lambda harder?
It can be hidden behind a lake/mountain and you have to make a program that goes around. :mountain:
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 :wink:
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).
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.
t
requires capability stack S
then {t}
requires empty : S
.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.
More generally, suppose that for each Swarm type tau
there is a corresponding (Haskell) type of capability analyses, C(tau)
.
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.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).
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).I have thought about this some more, and I seem to be coming to a few different (interrelated) conclusions.
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.
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.
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.
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.
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.
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
.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.cmd
types carry the requirements to execute the term.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.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.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 😄
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.
@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. 👍
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.
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.)
@byorgey could you please add that as a failing test case? 🙂
Describe the bug It seems that programs run by
base
are only checked dynamically for capabilities. This means that bothTo Reproduce
build "x" {move}; move
to see that the base builds the robot"x"
first before failing to execute themove
due to a missing capability. Ideally, it should instead refuse to run the entire program due to missing capabilities.The
build "x"
fails as it should with an error saying that you don't have the necessarily devices to install onx
(namely, a lambda and a strange loop). However, the last line works fine even though it shouldn't, since thebase
doesn't have a lambda or strange loop.