Loops

[effectfully]

Currently we unroll loops during parsing/typechecking. It's probably best to unroll them on the compiler side, since the compiler collects plenty of static info.

This means that we should try adding loops as primitives (i.e. constructors) to both the raw and the typed language. Loop bounds should be arbitrary expressions. The compiler will throw an error if it can't unroll a loop due to loop bounds not being static.

The previous issue talking about loops is #12.

[effectfully]

Loop bounds should be arbitrary expressions.

There's a major problem with this setup, though. Currently our strategy is to let the user write numbers and think of them as numbers, but lift those numbers into a finite field as well as all operations over them. This works fine as long as we don't need to "downcast" elements of the field into integers, which is what we do to compute comparisons, for example. This can be dangerous, for example, i * -1 <= 4 is false for i = 1.

In the same way it doesn't make much sense to downcast elements of the field to get integer bounds. No user expects 5 / 2 to evaluate to -26217937587563095239723870254092982918845276250263818911301829349969290592254.

Perhaps we want a separate type of integers that, say, all disappear during compilation. That could work for loop bounds at least (I doubt it's enough to get working comparisons, but I haven't spent any time investigating this issue).

[jakzale]

Maybe instead we should go for primitive recursion? Although I suspect that primitive recursion will be more difficult to use than loops.

What are loops actually used for in such language? Are they part of a spec?

[effectfully]

Maybe instead we should go for primitive recursion?

I don't have a feeling that it makes anything simpler, but who knows.

What are loops actually used for in such language? Are they part of a spec?

Kind of. See A.3.3.8 of the Sapling spec. We implemented that as ZKE.Field.Examples.ScalarMult.varBaseScalarMult. As you can see we need a loop there and we do use the loop variable.

Given that the language targets cryptographers we pretty much have to have loops, because this is what all those crypto algorithms use. Maybe just as a form of syntactic sugar on top of some kind of primitive recursion, though.

[effectfully]

This means that we should try adding loops as primitives (i.e. constructors) to both the raw and the typed language.

Seems to be done.

Loop bounds should be arbitrary expressions.

Tracked by #69.

i * -1 <= 4 is false for i = 1.

Should be fixed by #68 (the compiler is not updated yet, so can't check).

In the same way it doesn't make much sense to downcast elements of the field to get integer bounds. No user expects 5 / 2 to evaluate to -26217937587563095239723870254092982918845276250263818911301829349969290592254.

Perhaps we want a separate type of integers that, say, all disappear during compilation. That could work for loop bounds at least (I doubt it's enough to get working comparisons, but I haven't spent any time investigating this issue).

Not going to try that any time soon.

[effectfully]

I was thinking about loops and whether it's possible to have lexical scoping for them at all and I can't see a convenient way of making loops lexically scoped. Variables look to the user as if they were mutable, but internally every assignment creates a new variable, so they're immutable. So just declaring a variable outside of the loop and assigning it a value in the loop is not enough as it will create a new variable at each iteration. We could think of assigning the variable a value only once -- at the final iteration, but

1. you can't put a let into an if
2. even if you could, both branches of an if are evaluated, so that would still evaluate the assignment at each iteration

Although both of these problems can be fixed in this particular case, because statically computable things are supposed to have the usual semantics (if-expressions are lazy, for example). I haven't written a test for that statement yet, though (there's an issue in the compiler repo).

Another option would be to have a separate block in a for loop for things that happen after the loop finishes. Which is a bit weird, but could work.

Anyway, just being curious. Non-lexically scoped loops make sense in our case and that's what they use in the Sapling spec.

[effectfully]

One remaining problem with loops is what the value of i is after

for i = 1 to 10 do <...> end;

finishes. I like 11, @jakzale likes 10, but users will have arbitrary expectations, so such ambiguity is a problem regardless of what we choose in the end.

It perhaps would be best to remove i from the scope once the loop finishes.

BTW, what semantics, say,

for i = 1 to 10 do
    i = i + 1;
end;

is supposed to have?

[jakzale]

IMHO in the current implementation the cleanest semantics for for loops is as follows

• make the upper bound exclusive, as in Python ranges, and
• bind the variable after the loop to max start end.

@effectfully we do not really have variable assignments, just variable bindings, so the program will be written as

for i = 1 to 10 do
    let i = i + 1;
end;

Given the above, the semantics of the above loop are as follows:

• the loop gets evaluated 9 times for [1,10), and
• after the loop i is bound to 10.

Still, we should discuss about the following example

for i = 1 to 2 do
    let i = i + 2;
end;

as I am still unclear what i should be bound to after the loop.

I guess we could look into how SSA/LLVM handles for loops.

Finally, you mentioned that the compiler is using CPS, but as the language contains only bindings, it resembles SSA which is awfully similar to ANF which was touted as an alternative to CPS.

[effectfully]

IMHO in the current implementation the cleanest semantics for for loops is as follows

It's fine, but it doesn't matter if we go with this semantics or with some another one. What matters is to have loops that have an obvious semantics. Currently this is not the case. The easiest option would be just to dump for loops and use while loops, which have a very clear semantics, but then go explain to the user why you can't have an arbitrary computation in the loop header... Maybe we can reflect in the type of a variable whether the variable stores the result of a compile-time or runtime computation.

Or maybe we can use C-like for loops, which also have a clear semantics and forbid assigning anything to the loop variable in the body of the loop.

I'll think more on that, clearly there's a huge UX problem here.

we do not really have variable assignments, just variable bindings, so the program will be written as

Yeah, I just managed to forget the syntax.

Given the above, the semantics of the above loop are as follows:

• the loop gets evaluated 9 times for [1,10), and
• after the loop i is bound to 10.

That doesn't make any sense to me as I expect the loop counter to be incremented by virtue of it being a loop counter. I.e.

for i = 1 to 10 do end;

is already supposed to increment i automatically. So an additional i = i + 1 in the body should have some effect.

Finally, you mentioned that the compiler is using CPS, but as the language contains only bindings, it resembles SSA which is awfully similar to ANF which was touted as an alternative to CPS.

The compiler was using CPS for some technical stuff, but it was not the "compiling with CPS" technique, just some Cont sprinkled around to make certain things nicer much like we do in this repo. As of now, all Cont mentions are gone.

[jakzale]

Here is an interesting program, I suspect that is a bug in the renamer:

*** Failed! (after 646 tests and 23 shrinks):
        ERROR
          evaluation of the renamed program did not match the evaluation of the original program

        INITIAL STATE
          Env {unEnv = fromList [(26,Some 0)]}

        ORIGINAL PROGRAM
          for z_24 = 0 to -1 do
          let x_26 = x_26;
          end;
          let y_29 = if (0 == x_26) then 0 else 0;

        ORIGINAL PROGRAM FINAL STATE
          "[Some 0]"

        RENAMED PROGRAM
          for z_27 = 0 to -1 do
          let x_28 = x_26;
          end;
          let y_29 = if (0 == x_28) then 0 else 0;

        RENAMED PROGRAM FINAL STATE
          "VariableNotInScopeEvalError"

We probably should add an assignment operator, because at the moment renamer cannot tell apart a fresh binding with an assignment. We also need to unbind variables after for loop.

tack test --ta --quickcheck-replay=397135