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
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
