Static type-checking with dynamic scoping

Hi everybody,


        we couldn't find a clear answer to the following question and absolutely
need an answer, or a pointer to it:


        "Let's consider a Pascal-like imperative language, with dynamic
          binding of free variables inside abstractions (functions and
          procedures). Is it possible to perform static type-checking?"


We had a look to different books finding that languages using
the dynamic scoping rule either don't have types or perform
type checking at run-time, but that's not a negative answer.


We are developing an interpreter for the above language in prolog, using
a transition system as defined in "Plotkin - A structural approach to
operational semantics - Aarhus University, 1981".
He just mentions the existence of the dynamic scope rule, but gives
no answers on how it can be implemented.


In summary: is it possible to do static type-checking when you've dynamic
                        binding?
                        If not, are there restrictions on the language that makes it
                        possible (e.g. no recursion, no functional/procedural parameters)?


Thank you in advance


                                Roberto Alessandro
                                Bagnara Riaudo
--

Return to the comp.compilers page.
Search the comp.compilers archives again.