Can't use references in operators

[hmontero1205]

Only being able to use expression values in operators is not only inconvenient, but also limiting. For example, runtime/examples/clock.c has a while loop condition on an event variable. This currently cannot be expressed by the edsl.

[Rewbert]

The frontend EDSL is what's gotten the least attention so far.

I can change it to be of type SSM (Exp Bool) -> SSM () -> SSM (), so you can dereference variables etc in the condition for now. Koen & I will put our focus on the frontend after the vacation.

[Rewbert]

I've been thinking about this, and I have to say that I don't feel that it's right to allow references in expressions (loops aside).

Our references are somewhat like typed channels -- you can read from a channel, write to a channel, wait for a value to be placed in the channel etc. However, the value in these channels will change over time. What does it really mean to add two such channels together? What is the resulting value of this? Evaluating an expression should always yield the same result, but if the expression contains references, whose value can change over time, evaluating the same expression twice might give different results. If you form an expression you should be able to turn to that expression multiple times and expect the same result every time. If you need to talk about the values of references, I think it's only right that you sample the references for their value.

test :: Ref Int32 -> Ref Int32 -> SSM ()
test = box "test" ["x","y"] $ \x y -> do
  z <- var 0
  w <- var 0
  let sum = x + y
  z <~ sum
  wait [x]
  w <~ sum

After running this program we would expect z & w to have the same value, but since we waited for a change to x, the value of w could be different to that of z. I feel that it's right that we need to sample x and y before we refer to their values.

test :: Ref Int32 -> Ref Int32 -> SSM ()
test = box "test" ["x","y"] $ \x y -> do
  z <- var 0
  w <- var 0
  x' <- deref x
  y' <- deref y
  let sum = x' + y'
  z <~ sum
  wait [x]
  w <~ sum

Initially, the @-operator was a statement and not an expression, and this reasoning is why I designed it like that. If it's a statement the value must be sampled while evaluating the expression. Now we can form the @-expression and evaluate it multiple times, and get different results.

I agree that it's an eyesore but I don't think it warrants the change. It's still not tricky to understand what deref is doing, it's just not as nice on the eyes. I still think it's a good compromise to allow the while-condition to perform some side-effects, like reading from references, before returning a value.

[j-hui]

A statement like let sum = x + y shouldn't typecheck, at least in my vision, but I see your point.

In my mind, the dereference is still an explicit operation, but one that is performed inside of an expression rather than as a statement. So the program I have in mind should be:

test :: Ref Int32 -> Ref Int32 -> SSM ()
test = box "test" ["x","y"] $ \x y -> do
  z <- var 0
  w <- var 0
  let sum = deref x + deref y
  z <~ sum
  wait [x]
  w <~ sum

In my reading this, the let-binding just binds the syntactic representation of deref x + deref y, and can be used as syntactic sugar; it is different from assignment (i.e., <~). If the value of x or y changes after wait [x], then the value written to w will be different than what is written to z.

[Rewbert]

Hm okay, and yes perhaps my example was not the best as a let-binding would just bind a syntactic representation to a name.

I'll think about it a bit and see if I can collect my thoughts a bit until Tuesday. I am having trouble formulating my thoughts! My main concern here is that I want sampling of references to be explicit, which your example also has.

[j-hui]

I suppose here's a more concrete example (and closer to the kind of program @hmontero1205 was trying to write but couldn't):

f (b: &Bool) =
  while (*b)
    wait b

Without being able to dereference within an expression, we are unable to access the value of what b points to in the loop condition, in the EDSL:

f :: Ref Bool -> SSM ()
f b = do
  bv <- deref b
  while' bv $ do -- This just evaluates the initial value of b, and we have no way of modifying it
    wait [b]
    -- ???

It seems much more natural to write:

f :: Ref Bool -> SSM ()
f b = do
  while' (deref b) $ do
    wait [b]

We still explicitly dereference b here, but it takes place within the space of expressions rather than statements.

[Rewbert]

Yes it will just sample the value once, which is not expressive enough for us. I agree that we need to change it somehow