[bitc-dev] forall nesting

[Jonathan S. Shapiro]

> There is a more fundamental reason why you can't have a type
> like this, at least in any language that, like ML and Haskell,
> is based on the Hindley Milner type system:  forall quantifiers
> can only appear at the outermost level of a type, not nested
> inside a constructor, which is what you have done in the example
> above...

I understand the type logic behind this statement, but there is a
consistency issue here. Given a method such as less-than:

  < : (forall ('a : Num)  (fn ('a 'a) bool))

We can write at the top level prompt something like:

  (1:int32, <)

and we will get back something like:

  (forall 'a:Num (tuple int32 (fn ('a 'a) bool)))

however, note that this type had to be derived from an intermediate
step, which was:

  (tuple int32 (forall ('a:Num) (fn ('a 'a) bool)))

That is: the forall was hoisted to the outside by rewriting. This
suggests to me that there should be no syntactic difficulty with
allowing a syntactic form FORALL that introduces scoping of type
variables:

  (forall (tv1:constraint1 ... tvN:constraintN) type)

with the intended binding:

  (tyletrec ((tv1  constraint-1)
             (tvN  constraint-N))
    type)

[that is: type variables appearing in the constraints are scoped by type
variables defined within the FORALL] but with no implication of local
instantiation. That is, this is a convenience syntax, and it is
rewritten into a top-level forall by rewriting and alpha substitution.

I think what I am saying is that we can safely differentiate between the
SCOPE of the alpha variable and the EXTENT of the alpha variable. The
EXTENT must clearly be the top-level type, but I see no difficulty with
introducing scoping along something like these lines.


shap