Re: Procedure Parameters in Ada

Re: Procedure Parameters in Ada

[Donn Milton]

With reference to Chris Henrich's comments on type-checking in Pascal,
the Pascals I've seen only require that the type of the return
value be specified, such as:
		procedure dummy (function f: real);
There is no way to specify what the parameters to the formal function
'f' must be.  Thus although some type checking is possible, it is
IN GENERAL not possible to check that calls of f will always use the
correct parameters.  Recursive calls to a type-checking routine
won't hack it.

Please note:  the validity of the last sentence in the above paragraph
is by no means immediately obvious (at least to me).  One might
imagine the possibility of a type-checker that took into account
all possible execution paths of a program in order to check that all
procedures are always called with the correct number and type of
parameters.  But Langmaack, with a rather ingenious argument, shows
that such a type-checker cannot in fact be built (in the absence of
fully-specified procedure parameter types).

Donn Milton

Re: Procedure Parameters in Ada

[Donn Milton]

	
	>Ie. for the recursion above, couldn't something like
	>
	>	type procIrec = procedure ( integer i; procIrec p ) ;
	>
	>be permissible, and also stop the expansion of the type indefinitely?
	>And, more importantly, be distinct from
	>
	>	type otherprocIrec = procedure ( integer i; procIrec p ) ;
	>
	>which is structurally, but not name, equivalent.
	>
	>?
	>
	>
	>Andy "Krazy" Glew. Gould CSD-Urbana.
	
I have discussed constructs like this with some people, and can't find
any real holes in the idea.  I would certainly like to see this concept
considered for Ada '88.  Unfortunately, at that point, the impact that
such an addition would have on mature Ada compilers will have to be
a major consideration.

Donn Milton

Procedure Parameters in Ada

[Donn Milton]

Many people seem to be unaware of a major problem entailed by
procedures as parameters.  That is, when procedures are allowed
as parameters, strong type-checking becomes generally undecidable
(not just hard) UNLESS recursive mode-type declarations (a la Algol 68)
are introduced.  For example, in languages like Fortran, Algol 60,
PL/1, and C, strong type-checking cannot be done.  This was proved
formally by Langmaack in "On Correct Procedure Parameter
Transmission in Higher Programming Languages," Acta Informatica,
Vol. 2, 1973, pp. 110-142.

With the declaration mechanism available in Algol 68, it is possible
to declare "a procedure that has two parameters: an integer and a
procedure that has two parameters: an integer and a procedure that
has two parameters ..." ad infinitum, which is required for strong
type-checking of procedure parameters.  Understand that
type equivalence in Algol 68 means structural equivalence,
while type equivalence in Ada means name equivalence -- thus
type-checking is much simpler in Ada.

However, I do not understand why such a declaration mechanism, which
would allow procedures as parameters with strong type-checking,
was not included in Ada.  Algol 68 had demonstrated its
feasibility (with some elegance), and, as far as I know,
this capability is not a source of significant compile-time
or run-time inefficiencies.

Donn Milton

Re: Procedure Parameters in Ada

[aglew]

>With the declaration mechanism available in Algol 68, it is possible
>to declare "a procedure that has two parameters: an integer and a
>procedure that has two parameters: an integer and a procedure that
>has two parameters ..." ad infinitum, which is required for strong
>type-checking of procedure parameters.  Understand that
>type equivalence in Algol 68 means structural equivalence,
>while type equivalence in Ada means name equivalence -- thus
>type-checking is much simpler in Ada.
>
>Donn Milton

Thank you for the reference; I will have to chase it up. Please excuse
me, then, if I ask if type equivalennce by name is not possible in a
recursive type-mode system?

Ie. for the recursion above, couldn't something like

	type procIrec = procedure ( integer i; procIrec p ) ;

be permissible, and also stop the expansion of the type indefinitely?
And, more importantly, be distinct from

	type otherprocIrec = procedure ( integer i; procIrec p ) ;

which is structurally, but not name, equivalent.

?


Andy "Krazy" Glew. Gould CSD-Urbana.    USEnet:  ihnp4!uiucdcs!ccvaxa!aglew
1101 E. University, Urbana, IL 61801    ARPAnet: aglew@gswd-vms

Re: Procedure Parameters in Ada

[Chris Henrich]

[]
In article <8606042209.AA23350@vrdxhq.uucp> drm1@vrdxhq.UUCP (Donn Milton) writes:
>Many people seem to be unaware of a major problem entailed by
>procedures as parameters.  That is, when procedures are allowed
>as parameters, strong type-checking becomes generally undecidable
>(not just hard) UNLESS recursive mode-type declarations (a la Algol 68)
>are introduced.  

Procedure & function parameters are part of standard Pascal.
In the current ANSI/ISO standard (though not in the old book by
Jensen and Wirth) a certain degree of type checking is
mandated.  I know of at least one compiler which provides it.
It is not difficult; the routine which checks for
compatibility of types may have to call itself recursively.

These possibilities occur to me:
(a) what ANSI/ISO mandates is not "strong" in Donn Milton's
sense;

(b) something in Pascal corresponds to "recursive mode-type
declarations;

(c) for some other reason, the theorem being cited is beside
the point.

It may be worth while to note that subprograms as *variables*
have worse problems than subprograms as *parameters.*
Regards,
Chris

--
Full-Name:  Christopher J. Henrich
UUCP:       ...!hjuxa!petsd!cjh
US Mail:    MS 313; Concurrent Computer Corporation;
            106 Apple St; Tinton Falls, NJ 07724
Phone:      (201) 758-7288
Concurrent Computer Corporation is a Perkin-Elmer company.

Re: Procedure Parameters in Ada

[Jerry Sweet]

A sub-microscopic correction to what Chris Henrich said: Pascal
procedure and function parameters are described in Jensen & Wirth--at
least in the second edition.  See sections 9.1.2 and 10 of the Report.

-jns

Re: Procedure Parameters in Ada

[wf]

> 
> A sub-microscopic correction to what Chris Henrich said: Pascal
> procedure and function parameters are described in Jensen & Wirth--at
> least in the second edition.  See sections 9.1.2 and 10 of the Report.
> 
> -jns

The descriptions of *procedural* and *functional* parameters
(to use the correct terms) in Jensen & Wirth early editions
are NOT those of the BSI/ISO/ANSI standard.  There is now
a third edition of J&W which has been fully revised for compliance
with the ISO standard document by Andy Mickel and Jim Miner.
See sections 11.A.4 and 11.B.1 of the User Manual and section
11.3 of the "Report", *3rd edition*.

Re: Procedure Parameters in Ada

[Theodore S]

> []
 In article <8606042209.AA23350@vrdxhq.uucp> drm1@vrdxhq.UUCP (Donn Milton) writes:
>Many people seem to be unaware of a major problem entailed by
>procedures as parameters.  That is, when procedures are allowed
>as parameters, strong type-checking becomes generally undecidable
>(not just hard) UNLESS recursive mode-type declarations (a la Algol 68)
>are introduced.  
 
Chris Henrich writes that ISO [International Standards Org.]
Pascal has procedural & functional parameters and suggests.
> (a) what ANSI/ISO mandates is not "strong" in Donn Milton's sense;
> (b) something in Pascal corresponds to "recursive mode-type declarations;
> (c) for some other reason, the theorem being cited is beside the point.

I think the problem is that ISO Pascal puts some restrictions on which
procedures can be passed as arguments to which.  For example given
a procedure P, can P be passed as a procedure to itself i.e. P(P)?
In ISO Pascal the answer is no, in algol 68 it is yes.  This restriction 
is enforced mainly in the syntax. Which in ISO Pascal is:
	procheader ::= "procedure" name [ "(" formal {; formal} ")" ]
	formal     ::= ["var"] name ":" formal_type
		     | procheader | functionheader
Thus to write P's header we would have to say:
procedure P ( procedure Q (procedure R ( procedure S ... ad infinitum
which you can't since programmes must be of _finite_ length.

Perhaps the language for which Mr. Sherman wrote his complier is
the same way.  (I know that the Turing language developed at 
U. of Toronto is.)

In algol 68 you can just say (pardon my syntax):
type T = proc( T );   (* recursive type declaration *)
proc P( Q : T ) = <body of P>

Langmaak's paper (acta info. Vol 2) describes 4 languages, none of which
correspond to Pascal's way of doing things and one of which corresponds
to algol 68's. He proves that of the 4 only in the algol 68 like one can
full type checking be done at compile time.  Obviously this is also
true of the ISO Pascal way of declaring procedural parameters.
Thus the answer is (c), the theorem is just not relevant to Pascal.
But it is interesting, so thanks to Donn Milton for pointing it out.

					Theo Norvell
					norvell@utcsri