From: Matthias B. <bl...@re...> - 2001-09-26 18:41:55
|
Robert Harper wrote: > The possibility to use signature information to constrain declarations has > often been suggested, but it is difficult to put into practice. For > example, as you go along processing a structure, a binding for x might later > be shadowed, so any constraint on x's type in the signature would not affect > the earlier one. This makes it tricky to try to simultaneously type check a > structure and impose a signature on it. Thus most implementations that I am > aware of opt for synthesizing the principal signature of the structure, then > matching it against the target signature. However, this can have an > unpleasant effect of the kind you mention. I don't understand what the problem might be: If a variable's binding gets shadowed later, then whether or not its (tentative -- see below) type has a free type variable in it does not matter -- the compiler can simply choose an arbitrary type for that variable and no-one will ever know. (That's AFAIK the same situation as in "let val x = [] @ [] in 1 end" which is a perfectly valid SML program.) As for the simultaneous type-checking-and-constraint-applying approach: Why can one not work with unbound type variables (just like when type-checking a "let")? As I understand, that's what OCaml does. Of course, I do not agree with OCaml's solution of simply leaving unbound type variables in the final type; I have explained why. (It would not be a good idea in the context of separate compilation.) What I am suggesting here is to leave the variable _tentatively_ unbound. At the end of the day, when the whole topdec including all its signature constraints etc. has been considered and there are _still_ free type variables in the result, then we reject the program. But not before that. Matthias |