async as #286

xsebek · 2021-11-17T23:32:16Z

use the async library to check on as computation until it is done

Also get rid of `getRobotLoc` command since it is no longer needed.

byorgey · 2021-11-17T23:52:24Z

I don't know if you saw my other recent comment but I am skeptical of this whole approach. as will primarily (exclusively?) be used when checking win conditions for challenges. Such win condition checking programs are run to completion on every tick. So if an as command forks off a computation into another thread, it seems to me it won't help: the CESK machine will simply sit there busy waiting 8 ticks at a time until the computation in the other thread finishes.

And since the CESK machine for a win condition check is run in its own separate sub-call to runCESK, it won't even prevent the UI from freezing.

xsebek

Hey, @byorgey I got the background as to work 🙂

There a few things to iron out, mainly around printing, but the core of the change is pretty small (new async value, step (as&poll), IO cancel).

xsebek · 2021-11-17T23:34:35Z

src/Swarm/Game/Step.hs

+  VAsync (GAsync n1 _) -> \case
+    VAsync (GAsync n2 _) -> return $ compare n1 n2
+    VInt n2 -> return $ compare (fromIntegral n1) n2
+    v2 -> incompatCmp v1 v2


This is probably a bad idea as the VAsync value should be unobtainable anyway.

Yes, I don't think there is any reason for VAsync values to be comparable.

xsebek · 2021-11-17T23:38:26Z

src/Swarm/TUI/Controller.hs

+  (VtyEvent (V.EvKey (V.KChar 'c') [V.MCtrl])) ->
+    let cancel' = do
+          cm <- let m = s ^. gameState . robotMap . to (! "base") . machine in cancel m
+          pure (s & gameState . robotMap . ix "base" . machine .~ cm)
+     in continue =<< liftIO cancel'


Funny thing, I could not figure out how to make ix a Getter here or do the update in IO. 🤔

xsebek · 2021-11-17T23:44:08Z

src/Swarm/Language/Syntax.hs

+  | -- | Type for values that can not be directly created in code.
+    --   They are shown as e.g. @(__r1__)@, like C-style internal mangled
+    --   variables. With custom character it is slightly better then
+    --   using TInt.
+    TNonCode Char Int


@byorgey the name and printing is not great, but I did not want to create another TAsync here.

I changed it for VRef too, what do you think about it? 🙂

No, I don't like this. VAsync and VRef do not show up in the surface language, so there should not be a way to represent them in Syntax. Pretty-printing Values via valueToTerm was a horrible lazy hack in the first place; we should be trying to get rid of technical debt, not letting my lazy decisions in the past snowball into even more technical debt for ourselves. We should either just do something simple and stupid for now in valueToTerm for VAsync (like we were doing for VRef), or bite the bullet and write a proper Value pretty-printer.

xsebek · 2021-11-17T23:51:12Z

src/Swarm/Language/Typecheck.hs

@@ -384,6 +384,7 @@ infer s@(Syntax l t) = (`catchError` addLocToTypeErr s) $ case t of
    ty2 <- maybe id (`withBinding` Forall [] a) mx $ infer c2
    _ <- decomposeCmdTy ty2
    return ty2
+  TNonCode {} -> return UTyInt -- TODO: probably wrong, but I do not understand this code


@byorgey I might need a little help here 😕

There is nothing sensible to do here because there is no way to know what the type of a TNonCode is. Another reason that we should get rid of it. =)

xsebek · 2021-11-17T23:54:56Z

src/Swarm/Game/Step.hs

+
+        va <-
+          sendIO . Async.async $
+            either VString id -- TODO: that is not right...


This produces a wrong type on exception:

┌───────────────────────────────────┐ │ > as "base" {raise "tree"} │ │ "user exception: tree" : ∀ a1. a1 │ └───────────────────────────────────┘

But that should probably be solved with a better type of GAsync.

xsebek · 2021-11-18T00:20:31Z

@byorgey right, did not see your comment here 🙂

win condition checking programs are run to completion on every tick.

Sure, it is easy that way, but I thought the original idea was to delegate it to some invisible system robot?
That would allow multiple win conditions in a "do X, then do Y" style.
Also this makes it easy to add a time check, so that winning condition does not cycle.

the CESK machine will simply sit there busy waiting 8 ticks

I think it will only do a one pass over to poll function which will find the CESK is already finished - I only see delay with:

as "base" {wait 10000000} // waits once
as "base" {let f = wait 1; f in f}
testLIST_ALL // run "example/list"

Either way it should not stop us from making our godly robots more omnipotent and I do not see much overhead with this async change (we are passing around current immutable state, which is cheap). 👼

byorgey · 2021-11-18T17:37:34Z

Sure, it is easy that way, but I thought the original idea was to delegate it to some invisible system robot?

I think I considered that briefly but decided against it since I don't see much benefit, besides possibly saving a tiny bit of code because we already have code to run programs contained in robots. But in the end I think we would need a bunch of special cases either way. A win condition checker is fundamentally different than a robot.

Actually I'm not even sure I see how you could delegate the win checking to an invisible system robot. How would that work, exactly? What program would it run? Some kind of infinite loop? And how would it signal that you have won?

That would allow multiple win conditions in a "do X, then do Y" style.

Can you elaborate on how that would work? I am honestly curious, I can't imagine how it would work. Or at least I don't see how running the win condition checking in a special system robot vs as a separate program would make this any easier to support.

Also this makes it easy to add a time check, so that winning condition does not cycle.

Right, but to me this doesn't really seem like a problem worth solving.

byorgey · 2021-11-18T17:38:59Z

Stepping back, part of me thinks this is cool, but part of me wonders whether it is extra complication for little benefit. I would be happy to be wrong, but it feels to me like a solution without a problem. Can you explain exactly what problem this is supposed to be solving?

xsebek · 2021-11-18T18:49:07Z

@byorgey Thinking about it some more, your as is so generic already, that I think there is not much this brings to challenges directly. There is still the indirect benefit of making this REPL command less dangerous, which could come handy when testing.

Long term I would love to take advantage of more CPUs (CESK only runs on one) in game and the as command seemed as it could work and benefit from this change 🤔 I am kind of interested in this oracle power and what other time traveling is possible 🙂

Can you elaborate on how that would work?

I am not sure, but would the CESK machine in robot turn {cmd bool} into Up VBool? I kind of hoped we would put the robot inside and only check if it finished/restart it on failure.
If that did not work, I can imagine a more direct signalling with e.g. create "unlock part 1" or #212 style renameSelf "done".

With the more direct signalling, other robots could wait&check if others finished. My dream tutorial looks like this:

Robot R1 is waiting for the base to get tree, then it signals first check point is finished.
After that R2 takes over and checks for boat in inventory, then reprograms the base to move to another island and signals.
R3 then checks for stone and copper ore in inventory...

byorgey

I have tried to give some useful feedback even though I am still on the fence about whether it is worth merging this. I guess it is worthwhile seeing how good we can make this before making a final decision about merging it.

I am not sure it is a good idea to always run as in an async computation. Or perhaps we should have two versions, normal as which runs in an async computation, and unsafeAs which doesn't. However (vague brainstorming) it might also be cool to put this more in the user's control, i.e. some kind of built-in promise type with async and await commands...?

byorgey · 2021-11-19T14:28:09Z

src/Swarm/Game/CESK.hs

+  s' = resetBlackholes <$> getStore cesk
+  getStore :: CESK -> IO Store
+  getStore (In _ _ s _) = pure s
+  getStore (Out v s _) = (case v of VAsync (GAsync _ as) -> Async.cancel as; _ -> pure ()) >> pure s


This isn't guaranteed to cancel all currently running async computations, because there are lots of other places VAsync values could be hiding: in the environment, in a closure, ... I don't know how important this is. Perhaps not that important, since if an async computation keeps running but nothing ever asks for its value it only wastes some CPU cycles, it won't cause any crashes or anything like that. If it is important, we would have to do something like put references to currently outstanding async computations in the store, so that we can find them all when we want to cancel them.

I think I do not want to cancel all async computations - the ones currently being run by base are enough.

We could store the async values in GameState and add some way to cancel all of them in the UI.

byorgey · 2021-11-19T14:29:53Z

src/Swarm/Game/Step.hs

+        -- -----------------------------------------------------------------------------
+        -- TODO: move this code out
+        -- Slightly edited copy of Unit.hs version of runCESK:
+        let runCESK' :: CESK -> StateT Robot (StateT GameState IO) (Either Text Value)


Don't we already have this function in Step.hs? Hmm, or maybe that's only in my challenge-mode branch? Feel free to copy it: https://github.com/byorgey/swarm/pull/285/files#diff-bb4a5ea570cea9f815cdd1d92b33d4b6bd8daaa7d74c7014916c642c159e7d80R147-R173

Thanks, I will do so during rebase 🙂

byorgey · 2021-11-19T14:31:31Z

src/Swarm/Game/Step.hs


        -- Return the value returned by the hypothetical command.
-        return $ Out v s k
+        i <- gensym <+= 1
+        return $ Out (VAsync $ GAsync i va) s (FApp (VCApp Poll []) : k)


Conceptually, it probably makes more sense to make a new kind of Frame called FPoll rather than making Poll a primitive function.

I went the other way and made poll a real command. 🤷‍♂️

byorgey · 2021-11-19T14:36:09Z

src/Swarm/Game/Step.hs

+        mv <- sendIO $ Async.poll va
+        -- let mv = Nothing :: Maybe (Either SomeException Value)
+        let (msg, cesk) = case mv of
+              Nothing -> ("in progress", Waiting (time + 8) (Out (VAsync ga) s (FApp (VCApp Poll []) : k)))


I wonder if it makes sense to use some kind of exponential backoff (up to a maximum), e.g. if it hasn't finished after 8 steps, then the next time we wait 16, then 32, ... up to a maximum of 64 or something like that? For a long-running computation, checking every 8 time steps seems like a lot of polling, especially if we are writing to the robot log every time we check. We could put the waiting time to use as an argument of FPoll, i.e. FPoll n means "check if the async computation is done, and if not, wait n time steps until checking again".

I let await take int waiting period, but it would be fun to give it int -> int function instead 😄

byorgey · 2021-11-19T14:37:27Z

src/Swarm/Game/Step.hs

  VString t1 -> \case VString t2 -> return (compare t1 t2); v2 -> incompatCmp v1 v2
  VDir d1 -> \case VDir d2 -> return (compare d1 d2); v2 -> incompatCmp v1 v2
  VBool b1 -> \case VBool b2 -> return (compare b1 b2); v2 -> incompatCmp v1 v2
+  VInt n1 -> \case
+    VInt n2 -> return (compare n1 n2)
+    VAsync (GAsync n2 _) -> return $ compare n1 (fromIntegral n2)


I don't understand this at all. Why would we compare a VInt against the number in a GAsync?

byorgey · 2021-11-19T14:41:45Z

src/Swarm/Language/Syntax.hs

  deriving (Eq, Ord, Enum, Bounded, Data, Show)

 allConst :: [Const]
-allConst = [minBound .. maxBound]
+allConst = [minBound .. As] -- no Poll in code!


Right, see, this is telling us that we really should make poll a type of Frame instead of a Const. =)

I went full commands instead. 🙂

byorgey · 2021-11-19T14:44:40Z

src/Swarm/Language/Syntax.hs

+  | -- | Type for values that can not be directly created in code.
+    --   They are shown as e.g. @(__r1__)@, like C-style internal mangled
+    --   variables. With custom character it is slightly better then
+    --   using TInt.
+    TNonCode Char Int


No, I don't like this. VAsync and VRef do not show up in the surface language, so there should not be a way to represent them in Syntax. Pretty-printing Values via valueToTerm was a horrible lazy hack in the first place; we should be trying to get rid of technical debt, not letting my lazy decisions in the past snowball into even more technical debt for ourselves. We should either just do something simple and stupid for now in valueToTerm for VAsync (like we were doing for VRef), or bite the bullet and write a proper Value pretty-printer.

byorgey · 2021-11-19T14:46:56Z

src/Swarm/Language/Typecheck.hs

@@ -384,6 +384,7 @@ infer s@(Syntax l t) = (`catchError` addLocToTypeErr s) $ case t of
    ty2 <- maybe id (`withBinding` Forall [] a) mx $ infer c2
    _ <- decomposeCmdTy ty2
    return ty2
+  TNonCode {} -> return UTyInt -- TODO: probably wrong, but I do not understand this code


There is nothing sensible to do here because there is no way to know what the type of a TNonCode is. Another reason that we should get rid of it. =)

byorgey · 2021-11-19T14:47:46Z

src/Swarm/Language/Typecheck.hs

@@ -476,6 +477,7 @@ inferConst c = toU $ case c of
  Exp -> arithBinT
  AppF -> [tyQ| (a -> b) -> a -> b |]
  As -> [tyQ| string -> {cmd a} -> cmd a |]
+  Poll -> [tyQ| cmd a |] -- TODO: poll is NOT exported as command


Right, Poll does not have any sensible type---yet another reason it should be a Frame instead of a Const.

byorgey · 2021-11-19T14:49:12Z

src/Swarm/TUI/Controller.hs

+handleREPLEvent s = \case
+  (VtyEvent (V.EvKey (V.KChar 'c') [V.MCtrl])) ->
+    let cancel' = do
+          cm <- let m = s ^. gameState . robotMap . to (! "base") . machine in cancel m


Using (! "base") will crash if there is no robot named "base" which is a big no-no! I will have to think about how to rewrite this code.

Well I have no idea, let me know if you think of something 😉

I mean one simple thing is just to wrap this in a check: first check if the robotMap has a key "base" and if so do the cancelling stuff.

byorgey · 2021-11-19T15:07:02Z

Long term I would love to take advantage of more CPUs (CESK only runs on one) in game

Agreed! Though I think we could also do this more simply by running multiple robots in parallel.

I am not sure, but would the CESK machine in robot turn {cmd bool} into Up VBool? I kind of hoped we would put the robot inside and only check if it finished/restart it on failure.

Yes, that would work, but it would mean we have to specially handle that robot to check its return value and restart it. We wouldn't really get much benefit from treating it as a robot as opposed to just a special standalone CESK machine.

Robot R1 is waiting for the base to get tree, then it signals first check point is finished.
After that R2 takes over and checks for boat in inventory, then reprograms the base to move to another island and signals.
R3 then checks for stone and copper ore in inventory...

Yes, this sounds really cool, but I wonder if we could do this more simply by adding a mechanism for mutable state, aka "static variables". If there is a CESK machine we run on every tick, when it notices that the first check point is finished, it sets a mutable variable in the store; when we run it on the next tick, we pass the same store to it so it can have state that persists across runs. It then sees that the first checkpoint is complete so it only checks for the second checkpoint, and so on.

For entities that should always be drawn as if the robot knows what they are. Mostly useful in creating challenge scenarios.

Co-authored-by: Ondřej Šebek <[email protected]>

We don't actually need an enumeration type for different game types. There are really several orthogonal things going on: 1. How the world, robots, inventory, etc. are initialized. 2. Whether there is a winning condition. 3. Whether we are in "creative mode", allowing the player to do anything they want.

xsebek · 2021-11-25T15:06:42Z

@byorgey I went with the future type and async, await, poll and cancel commands:

_{(Oops, the poll type is actually wrong, let me fix that...)}

xsebek · 2021-11-25T18:39:27Z

Hmm, await does not really work - it does not get run again by the machine and instead return after waiting once:

> a <- async "base" {testLIST_ALL; return 1}; await a
await async {force testLIST_ALL; return 1} : int

> def await0 = \f. e <- poll f; case e (\u. await0 f) return; end
> a <- async "base" {testLIST_ALL; return 1}; await0 a
1 : int

I tried with changing it to functionLow and it did not help 😕
Maybe the second form is not that bad and await is not really needed.

byorgey · 2021-12-01T16:23:19Z

src/Swarm/Game/Step.hs

  VUnit -> \case VUnit -> return EQ; v2 -> incompatCmp VUnit v2
  VInt n1 -> \case VInt n2 -> return (compare n1 n2); v2 -> incompatCmp v1 v2
  VString t1 -> \case VString t2 -> return (compare t1 t2); v2 -> incompatCmp v1 v2
  VDir d1 -> \case VDir d2 -> return (compare d1 d2); v2 -> incompatCmp v1 v2
  VBool b1 -> \case VBool b2 -> return (compare b1 b2); v2 -> incompatCmp v1 v2
+  VAsync _ a1 -> \case VAsync _ a2 -> return $ compare a1 a2; v2 -> incompatCmp v1 v2


I don't really think comparing VAsync values makes much sense. What would you use this for? And what would it mean for one to be less than another?

byorgey · 2021-12-01T16:26:03Z

src/Swarm/Game/Value.hs

  deriving (Eq, Show)

+-- | Type for asynchronous computation which may raise an Exn.
+newtype GAsync a = GAsync {asyncComp :: Async.Async (Either Exn a)}


Do we really need the GAsync type? What's the benefit of defining GAsync as opposed to inlining its definition directly into VAsync (i.e. VAsync :: Term -> Async.Async (Either Exn Value) -> Value)? It kind of feels like unnecessary indirection to me.

byorgey · 2021-12-01T16:29:55Z

src/Swarm/Language/Syntax.hs

@@ -530,6 +544,10 @@ pattern TBind v t1 t2 = SBind v (STerm t1) (STerm t2)
 pattern TDelay :: DelayType -> Term -> Term
 pattern TDelay m t = SDelay m (STerm t)

+-- | Match a TDelay without syntax


This comment needs to be updated.

What is the purpose of SFuture / TFuture? It seems like it can never actually result from parsing surface syntax, right? Is it only for pretty-printing values? As I think I mentioned before I really don't want to add extra stuff to the AST just to be able to pretty-print values.

byorgey · 2021-12-01T16:31:47Z

src/Swarm/Language/Syntax.hs

    As
+  | -- | Hypothetically run a command as if you were another robot,


async doesn't actually have the sense of "as if you were another robot", does it?

byorgey · 2021-12-01T16:32:51Z

src/Swarm/TUI/Controller.hs

+handleREPLEvent s = \case
+  (VtyEvent (V.EvKey (V.KChar 'c') [V.MCtrl])) ->
+    let cancel' = do
+          cm <- let m = s ^. gameState . robotMap . to (! "base") . machine in cancel m


I mean one simple thing is just to wrap this in a check: first check if the robotMap has a key "base" and if so do the cancelling stuff.

byorgey · 2021-12-01T16:36:10Z

src/Swarm/Game/Step.hs

+        time <- use ticks
+        mv <- sendIO $ Async.poll a
+        return $ case mv of
+          Nothing -> Waiting (time + 8) (Out va s (FApp (VCApp Await []) : k))


I think an FExec is needed, so that the Await is re-executed once it is applied.

Suggested change

Nothing -> Waiting (time + 8) (Out va s (FApp (VCApp Await []) : k))

Nothing -> Waiting (time + 8) (Out va s (FApp (VCApp Await []) : FExec : k))

xsebek · 2022-06-30T19:34:01Z

I do not think we need this now, but if we ever want to explore this direction we can look here for tips. 🙂

byorgey added 22 commits October 29, 2021 17:48

initial Challenge data type representing challenges

ae84d9f

add getRobotLoc command

03706c7

basic loading of challenges

a61542f

winning conditions

6fc48cb

Merge branch 'main' into challenge-mode

f41a773

fix merge

7ff3364

fix coords of sample challenge mode world

b17d0f5

tweak starting devices for sample challenge

39bf5dd

WIP: work on parsing challenges from .yaml files

f31e17d

WIP: a bit of progress on parsing challenge robot list

c7bce62

framework for parsing YAML that depends on EntityMap

14fc694

fix tests

791aa04

fix warnings

60bc572

basic ability to load a challenge from the command line

1f596aa

built robots head east if parent has dir of zero

ff76875

allow program to be omitted in YAML robot description

4351475

parse world descriptions in challenges

5a40c6e

add 'as' command for hypothetical evaluation as another robot

b8b923e

Also get rid of `getRobotLoc` command since it is no longer needed.

get benchmark compiling again

4f7ed89

add a basic modal pop-up when the user wins a challenge

b7d8258

allow defining custom entities in challenges

b67d126

generalize robot descriptions for challenges

8937faf

xsebek requested a review from byorgey November 17, 2021 23:32

xsebek commented Nov 18, 2021

View reviewed changes

byorgey requested changes Nov 19, 2021

View reviewed changes

byorgey and others added 14 commits November 19, 2021 09:32

add known property

c29e153

For entities that should always be drawn as if the robot knows what they are. Mostly useful in creating challenge scenarios.

first tutorial challenge?

83e91e7

rename 'codex' to 'challenge'

3c778f0

get rid of outdated testing challenge

37d6e97

Fix inventory for move challenge

352330a

Co-authored-by: Ondřej Šebek <[email protected]>

Update error message when parsing ProcessedTerm

a930851

Co-authored-by: Ondřej Šebek <[email protected]>

add boolean to Won instead of repurposing NoWinCondition

0dae572

fix unit test

1511955

challenges can now be loaded from relative or absolute location

4ca5567

fix benchmark

a44da3f

rename item from 'challenge' to 'goal'

39a17ad

test parsing all challenges in data/challenges

07c2064

add move2 challenge

0623c07

xsebek force-pushed the async-as branch from de2838d to 4e09c1e Compare November 25, 2021 15:02

xsebek added 2 commits November 25, 2021 18:21

Async is the future

a2653c6

Fix types

d31e92e

xsebek force-pushed the async-as branch from 4e09c1e to d31e92e Compare November 25, 2021 18:34

byorgey requested changes Dec 1, 2021

View reviewed changes

byorgey reviewed Dec 1, 2021

View reviewed changes

Base automatically changed from challenge-mode to main January 27, 2022 23:00

xsebek closed this Jun 30, 2022

		As
		\| -- \| Hypothetically run a command as if you were another robot,

	Nothing -> Waiting (time + 8) (Out va s (FApp (VCApp Await []) : k))
	Nothing -> Waiting (time + 8) (Out va s (FApp (VCApp Await []) : FExec : k))

async as #286

async as #286

Conversation

xsebek commented Nov 17, 2021

byorgey commented Nov 17, 2021 • edited Loading

xsebek left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xsebek commented Nov 18, 2021 • edited Loading

byorgey commented Nov 18, 2021

byorgey commented Nov 18, 2021

xsebek commented Nov 18, 2021

byorgey left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

byorgey commented Nov 19, 2021

xsebek commented Nov 25, 2021

xsebek commented Nov 25, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xsebek commented Jun 30, 2022

byorgey commented Nov 17, 2021 •

edited

Loading

xsebek commented Nov 18, 2021 •

edited

Loading