[bitc-dev] Poll: FORALL syntax

[Jonathan S. Shapiro]

Right now, the forall syntax appears *inside* its corresponding defining
form:

  (defstruct (forall ((IntLit 'a)) (mystruct 'a))
    field : 'a)

It is also somewhat irregular, because in appears in the "type" position
in DEFINE and PROCLAIM, and can be attached to any identifier pattern:

  (define (f x:(forall ((Arith 'a)) 'a) y:'a)
    (+ x y))

Because of this odd irregularity, I am considering moving the forall
form to the outside. The examples above would now be written:

  (forall ((IntLit 'a))
    (defstruct (mystruct 'a) field : 'a))

  (forall ((Arith 'a))
    (define (f x:'a y:'a) (+ x y)))

I personally find it more comprehensible to have the constraints
gathered together in one place, and not in the middle of other parts of
the definition syntax. Also, the syntax reflects the qualification more
accurately, because the "scope" of the qualifier is the top level
definition. [We'll need to do something sensible with LET as well.]

Does anyone object if FORALL moves to the outside in this way? Other
options? Opinions?


shap