PEP 3107 and stronger typing (note: probably a newbie question)

[Bruno Desthuilliers]

Paul Rubin a écrit :
> Bruno Desthuilliers <bdesth.quelquechose at free.quelquepart.fr> writes:
> 
>>>    [A type system is a] tractable syntactic method for proving the
>>>    absence of certain program behaviors by classifying phrases
>>>    according to the kinds of values they compute. (Pierce 2002)."
>>
>>Is this supposed to contradict my assertion that *static* typing is
>>for compilers ?
> 
> Yes, the main benefit these days is to prove the absence of certain
> types of bugs in the program.

As someone said, if declaring types thrices was enough to ensure 
correctness, I'd happily do so.

I still maintain that the primary *practical* reason behind static 
typing is to provide optimization clues for the compiler. You can (or at 
least could) have declarative static typing with very few type 
*checking* - I may be wrong here but I think one could even write a C 
compiler without *any* type checking. Heck, the programmer said it's a 
char*, so it must be one, right ?-) Of course, no one in it's own mind 
would use such a compiler (if you have to suffer from the restrictions 
imposed by static typing, you want to also profit from it's benefices - 
or at least avoid the possibly dramatic effects of a type error in these 
systems). Also, some (mostly) dynamically typed languages have grown 
type-annotations for the very same reason : hinting the compiler about 
possible optimizations.

wrt/ proofs of correctness, I'll just point to the spectacular failure 
of Ariane, which was caused by a *runtime* type error in a system 
programmed in ADA - one of the languages with the most psychorigid 
declarative static type systems. Not to say these proofs are inexistant, 
just that they are IMHO a bit overvalued - at least wrt/ to my daily 
concerns. Most of the errors I have to deal with are logical errors, not 
type errors, and given the kind of "logic" (err...) you can find in 
business applications (to make a long story short : it has very few to 
do with mathematics), I have some doubt about what a static type system 
- even a _very_ smart one - could prove here, at least if we hope to 
deliver the application within time and budget constraints (sorry for 
being soo practical here).

> The article "What To Know Before Debating Type Systems" is pretty
> informative (though it doesn't go as far as to call C/C++ untyped):
> 
>    http://cdsmith.twu.net/types.html

Quote :
"""
Therefore: I give the following general definitions for strong and weak 
typing, at least when used as absolutes:

     * Strong typing: A type system that I like and feel comfortable with
     * Weak typing: A type system that worries me, or makes me feel 
uncomfortable
"""

According to this definition, I herefore declare that Python is strongly 
typed and Java weakly typed !-)

(sorry, couldn't resist).

More seriously, it's indeed an interesting article - even if I do not 
necessarily share all the views of the author - for those not knowing 
anything about type systems. But it's clearly a bit oriented and IMHO 
fails to present the pros of dynamic typing.

BTW, if I may insert another quote, that I think is relevant here as 
well as in another recent thread about 'typed' containers in Python:
"""
I find it amusing when novice programmers believe their main job is 
preventing programs from crashing.  I imagine this spectacular failure 
argument wouldn't be so appealing to such a programmer.  More 
experienced programmers realize that correct code is great, code that 
crashes could use improvement, but incorrect code that doesn't crash is 
a horrible nightmare.
"""

> 
>>>C and C++ are basically untyped languages.
>>
>>Hem... This assertion is at least debatable. Care to post this on
>>c.l.c or c.l.c++, so we get some feedback ?
>  
> I wouldn't consider the aficionados of those dinosaur languages

Hmmm... For a dinausor, C seems well alive. Can you remind me which 
language is used to implement CPython and most of actual operating 
systems and low-level libraries ?

> to be
> authorities on such a question.

If you mean that most them aren't necessarily great CS theorists, then 
you may be right. OTHO, they do have some practical experience with 
these languages, so they might have something to say...