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

[Bruno Desthuilliers]

Paul Rubin a écrit :
> Bruno Desthuilliers <bruno.42.desthuilliers at wtf.websiteburo.oops.com> writes:
> 
>>Nope, he just asserted something wrong. Static typing is for compiler
>>optimization. Type checking is at most a side effect, and in some
>>languages (at least C, C++ and Java) can be totally defeated (usually
>>using typecasting).
> 
> 
>   "Definitions of type system vary, but the following one due to
>   Benjamin C. Pierce roughly corresponds to the current consensus in
>   the programming language theory community:
> 
>     [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 ?

C (and C++) are statically typed. It's usually agreed that C is weakly 
typed, and that C++ is somewhat more strongly typed. In both cases, you 
can totally defeat compile-time type-checking, with possibly some very 
unpredictable results. Python is dynamically typed, but doesn't allow 
the kind of results you can get from a C typecast.

>   -- http://en.wikipedia.org/wiki/Type_theory#Type_system



> 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 ?

> Java casts can only
> partially defeat its type system,

In Java, an erroneous typecast will result in a runtime error. Where's 
the benefit of static typechecking if you can get type errors at runtime?