drm1@vrdxhq.UUCP (Donn Milton) (06/05/86)
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
aglew@ccvaxa.UUCP (06/08/86)
>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
drm1@vrdxhq.UUCP (Donn Milton) (06/09/86)
>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
cjh@petsd.UUCP (Chris Henrich) (06/09/86)
[] 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.
jsweet@ICS.UCI.EDU (Jerry Sweet) (06/10/86)
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
drm1@vrdxhq.UUCP (Donn Milton) (06/11/86)
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
wf@glasgow.UUCP (06/13/86)
> > 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*.
norvell@utcsri.UUCP (Theodore S) (06/13/86)
> [] 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