[net.lang.ada] misleading article on type checking procedure parameters

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