C strongly typed?

[William E. Aitken]

In article <8356 at pt.cs.cmu.edu> flc at n.sp.cs.cmu.edu (Fred Christianson) writes:
>In article <4401 at hydra.Helsinki.FI> grano at cs.Helsinki.FI (Kari Gran|) writes:
>>a strictly (strongly? - not well defined terms anyway) typed language. 
>
>Here's ONE POSSIBLE definition.  I'm not arguing that "strongly typed" is
>well defined. I'm just giving one definition.
>
>From Aho, Sethi and Ullman's _Compilers,_Principles,_Techniques,_and_Tools_:
>
>	A language is strongly typed if its compiler can guarantee that 
>	the programs it accepts will execute without type errors ...
>
>	For example if we first declare
>		
>		table: array[0..255] of char;
>		i: integer
>	
>	and then compute table[i], a compiler cannot in general guarantee
>	that during execution, the value of i will lie in the range 0 to 255.
>
>The C equivalent example
>
>	char	table[256];
>	int	i;
>
>shows that C is not "strongly typed" according to Aho, Sethi, and Ullman.

I don't see how, evaluation of table[i] is not a type error but a subscript
out of range error (incidentally, the same thing happens in Pascal
which is (I believe) generally considered strongly typed).  If you
think that I am splitting hairs here, consider the case of zero division.  

I submit the thesis that there is no good definition of strongly typed.

Some authors have used it to mean statically typed.  I.e. all expressions
and sub expressions have types determinable at compile time.  This admits 
languages with a single type to which all objects belong.  This is hardly 
satisfying.

We have already seen that the definition given above is easily defeated 
by declaring, by fiat, that all run time errors are not type errors.

Another possibility is to say that no run time errors will occur.  This
is easily confounded by the language that is defined to enter a tight 
infinite loop whenever it detects a run time error.  (another possibility 
is to raise an exception, and provide a default handler)

Outlawing these devices compromises either compilability or expressiveness:
either the acceptability of a given program is no longer decidable, or
the language is no longer Turing-complete, or both. 

When evaluating type systems, several issues must be addressed.

	(1) Is well-typing decidable?
	(2) Is well-typing compile-time decidable?
	(3) What run-time guarantees are there for well-type programs?
	(4) Are run-time checks required? how expensive are they?
	(5) How expressive is the type system?  That is what
	    properties of data can one express with types.
	(6) How restrictive is the type system?  What programs can I write?

The relevence of many points raised in this debate hinges on whether 
the expressive of a type system has anything to do with its ``strength''.

I have rambled on for too long

						--- Bill.
William E. Aitken <aitken at cs.cornell.edu>   | On Earth it is considered 
{uw-beaver,rochester,decvax}!cornell!aitken | ill mannered to kill your
Home: (607) 273-7810 Away : (607) 255-9206  | friends while commiting suicide
============================================*============= Avon ==============