[bitc-dev] Syntax of FORALL

[Jonathan S. Shapiro]

As we re-syntax the language, I did something by accident in a private
email that has been sticking in my mind, and I would like input on it.

For type qualification in the S-expr syntax, we chose FORALL, but as we
introduce preconditions and postconditions the forall syntax may become
confusing.

The other day, I unthinkingly wrote REQUIRE instead, as in:

  REQUIRE Eql('a) IN
  DEF ReallyEquals(x:'a, y) x == y;

where Eql here is a type class (note this is block syntax). Swaroop was
uncomfortable with this use of REQUIRE, because require is more
traditionally used for preconditions.

But the more I think about it, the more I feel subjectively that type
constraints *are* a form of precondition (or on the return type,
postcondition). They simply happen to be one that is statically
resolvable. Given this, I wonder if it doesn't make perfectly good sense
to be able to write something like:

  REQUIRE IntType('a), x > 0 IN
  DEF fact(x) x * fact(x - 1);

Note, in particular, that this has the side effect of reserving FORALL
for use in expression preconditions and postconditions.

I would appreciate reactions. Do people find this confusing, pleasing,
pleasing after some initial surprise, outright wrong, or just plain
silly?


shap