run prints value with bogus type

[byorgey]

Describe the bug
Calling run on certain files causes the result of executing the file to be printed along with a unit type, regardless of the actual type of the result.

To Reproduce
In true.sw:

true

Now start swarm and at the REPL, type run("true.sw") This will print out

true : ()

Expected behavior
It should result in

true : bool

(or perhaps it shouldn't print anything at all?).

[byorgey]

Another odd thing which seems related:

> if true {move; move} {move}
> if true {x <- move; move} {move}
() : ()

Both execute normally, but in the first case nothing is printed, whereas in the second case () : () is printed. I think it has something to do with binds generating a VResult, which is also related to #327 .

[byorgey]

When an expression is entered at the REPL, we first store its type by setting the replStatus to REPLWorking ty Nothing. Then once the CESK machine finishes we take the value that results and print it out along with the type. So the type of run("foo.sw") is cmd () (there is a special case that strips off the cmd before printing the type). But the problem is that run("foo.sw") basically replaces itself so that we actually evaluate the contents of the file foo.sw; but the type in the replStatus never gets updated.

...I guess this means run actually breaks type preservation! The more I think about it the less I like run and the way it currently works. It's expedient but not very well-motivated theoretically.

[byorgey]

I also encountered () : () being printed when defining a function that called build and did a few other things, then calling that function at the REPL prompt.

[byorgey]

To be clear at this point, I am keeping this open so we remember that it's a problem, but I expect it will be completely and properly solved by #495, so this issue is not worth working on in and of itself.

[xsebek]

Fun idea, would it make more sense for run to have type cmd a?

Then you could at least use the return value at your own risk.

[byorgey]

I don't see how that would be better. It would still be wrong, and you can already use the return value at your own risk.

[xsebek]

@byorgey no, you can only use it as a result of the whole computation (e.g. in objective #828), not in the same term.

Consider this file coinflip.sw:

b <- random 1;
if (b == 0) {
    r <- run "coinflip.sw";
    return $ r + 1; // <-- this r does not type check, because it is unit
} {
    return 0;
}

[byorgey]

Ah, good point. Still, I don't really see the benefit. I'd rather just do it properly and implement #495. In fact that is one of the next things I was thinking of working on.

[byorgey]

Also related is #1087 which will hopefully get rid of all the VResult machinery.