syndicate-2017/doc/notes-on-hll.md

Syntax

Just a sketch, at the moment.

Instantaneous actions, I := (actor I ...)
                            (network I ...)
						    (state [B O ...] [E I ...] ...)
							(background I ...)
							(assert! P)
							(retract! P)
							(send! P)
							(flush!)              ;; ???
							expr
    Optional Bindings, B := ;; nothing, or
		                    #:collect [(id I) ...]
	  Ongoing actions, O := (on E I ...)
							(once E I ...)        ;; ???
							(assert P)
							(assert #:when Pred P)
							(track [x Agg] I ...)
							(begin O ...)         ;; ??? begin isn't quite right
		Predicates, Pred := (not Pred)        ;; -- NOT YET IMPLEMENTED
							(exists P Pred)   ;; -- NOT YET IMPLEMENTED
							(forall P Pred)   ;; -- NOT YET IMPLEMENTED
							expr
			   Events, E := (asserted P)
							(retracted P)
							(message P)
							(rising-edge Pred)
							(falling-edge Pred)
         Aggregates, Agg := (count expr P)
		                    (set expr P)
							(hash k_expr v_expr P)
							(project P)
							(single-value expr P)
							(single-value expr P #:default def_expr)
							Pred
             Patterns, P := ... ;; uses $var as binder

(define-syntax-rule (until B E O ...)
  (state [B O ...] [E (final-values-of B)]))

(define-syntax-rule (forever B O ...)
  (state [B O ...]))

Note also that falling-edge is encodable using rising-edge and not, and that forall is encodable using exists and not.

state has the B bindings visible in the Is, and returns the value of the final I from the E exit branch that was chosen.

There are four kinds of actor-spawning Is: actor, network, state and background. Neither actor, network nor background yield a value; only state does so. However, both state and background link to their invoking contexts, because state may return a value or crash, and background may crash. Actors using state and background must therefore have a special continuation table in their private state to link them to their state and background logical-children-but-physical-siblings. The link communicates values (on success) and crashes (on failure).

Q: Should exception values be transmitted on state failure? I think no, but I am not sure there's a good reason why not.

Of the events, asserted, retracted and message require no private-state, since the network does the book-keeping for us. rising-edge, however, needs to track the state of its predicate. If the predicate happens to involve an exists, then an assertion set must be maintained, like for a track.

This is leading me to believe that the order of operations is:

• Given a patch,
  • update tracks and assertion-sets related to rising-edge.
  • handle on for asserted, retracted and rising-edge, in order of appearance
  • check termination conditions
  • maintain asserts and subscriptions for ons
• Given a message,
  • handle on for message and rising-edge, in order of appearance
  • check termination conditions
  • maintain asserts and subscriptions for ons

Actually, I'm not sure falling-edge is encodable using rising-edge, since the initial state might be different. Do we assume that the level is high when the level is unknown for a falling-edge? I think it likely, given I think it likely that we assume the level is low when the level is unknown for a rising-edge.

when is a bit tricky, because it should clearly apply to on and assert, but it is not clear that it should apply to track. Furthermore, what should happen if, mid-way through some interaction involving assertions, the when predicate goes false? Should the subscription be retracted? On balance, I'm starting to think that when is a bad idea. In my sketches so far, there's only one place it's used, to conditionally assert a set, so I've added #:when to assert instead.

Note that exists (and so forall) are tricky because of the nested Pred. For now, I'm not implementing them -- we'll see how painful it is to use track and plain-old expr Preds instead.

Examples

#lang prospect/actor
;; Simple mutable box and count-to-infinity box client.

(struct set-box (new-value) #:transparent)
(struct box-state (value) #:transparent)

(actor (forever #:collect [(value 0)]
         (assert (box-state value))
         (on (message (set-box $new-value))
           new-value)))

(actor (forever
         (on (asserted (box-state $value))
           (send! (set-box (+ value 1))))))