ms1g@ANDREW.CMU.EDU (Mark Steven Sherman) (06/09/86)
I felt very uneasy about the claim that procedure parameters/variables cannot be typed checked at compile time, since 1) I had written a compiler that purported to do that and 2) there is a widely publicized result by Ed Clarke to the effect that if one has *all* of procedure parameters, global variables, static scope, recursion and something else (I think reference parameters), then one cannot create a sound, complete axiomatic description of the language (in the sense of Cook) but if you drop one of those requirements, then you can. Naturally, the referenced Acta Informatica article implied that 4 of Clarke's conditions were superflous -- if you can't type check it, you can't prove it. So I looked up the article. It says something much, much weaker, and uses 30 pages of formalisms to demonstrate, to my mind, the obvious. The property of Algo-60 (and purported property of PL/1) that makes it impossible to type check is that procedure parameters (there are no procedure variables in Algol-60) do not have their formal parameters specified anywhere -- with the trivial exception of return types, you merely say that an identifier denotes a procedure -- of course one can't guarantee type correctness. I submit the following pseudo-Algol-60 demonstration program which I hope Acta Informatica will publish as soon as they can: begin comment "formality" ; boolean procedure CheckHalt(TuringIndex);@* integer TurindIndex@* begin@* comment Insert your favorite turing machine simulator ;@* if halts return true else return false;@* end; comment procedure that will fail as necessary; procedure test(q);@* procedure q;@* begin@* q(1)@* end; comment Two different possible parameters; procedure p1; begin write("Lose") end; procedure p2(i); integer i; begin write("Win",i) end; comment Value to read; integer WhichMacine; read(WhichMachine);@* if CheckHalt(WhichMachine) then test(p1) else test(p2) end I'll even change the input to a constant -- you give a compiler that can tell me if this program generates a runtime (type check) error, and I'll solve the halting problem. By the way, the PL/1 compiler I have been using for the last three years does indeed require that I specify parameter and return types for all entries, including nested entries, which meets the requirements of the article. Note: there is no need to distinguish name equivalence and structural equivalence. The article only talks about completely specifying the parameters or not. (By the way, the reason the artcile is so long is that it actually considers four classes of languages: 1) nothing about procedures' signatures needs to be specified, 2) only the return type needs to be specified, 3) return types and parameters need to be specified, but not nested procedure parameters, i.e., the procedure parameter must list its arguments, but if one of those arguments is also a procedure parameter, then the most nested parameter need not be specified, and 4) everything specified. I'll bet you're not surprised that the results are pretty much the same for languages 1-3.)
drm1@vrdxhq.UUCP (Donn Milton) (06/10/86)
The key point is that parameters need to be fully specified, to to an arbitrary (and not necessarily finite) degree of nesting, in order to permit full type-checking. This requires some sort of recursive type definition for procedures. Sherman claims that he has written a compiler that performs full type-checking, presumably in the absence of fully specified procedure parameters. I would be very interested in hearing more about such a compiler, since so far Langmaack has convinced me it is impossible. I do not have the reference to Clarke's result, but from the description it is does not conflict with Langmaack, as long as Clarke was referring to "fully-specified procedure parameters." I also do not understand the point of the program that Sherman presented, for which he states "you give a compiler that can tell me if this program generates a runtime (type check) error, and I'll solve the halting problem." The crux of strong type-checking is that it is done at compile-time and not at run-time. The program should generate a compile-time error -- it is irrelevant whether the particular portion of the program that contains the error would be executed at run-time. Donn Milton