Python from Wise Guy's Viewpoint

[Joachim Durchholz]

Andrew Dalke wrote:
> Pascal Costanza:
> 
>>The set of programs that are useful but cannot be checked by a static
>>type system is by definition bigger than the set of useful programs that
>>can be statically checked. So dynamically typed languages allow me to
>>express more useful programs than statically typed languages.
> 
> Ummm, both are infinite and both are countably infinite, so those sets
> are the same size.  You're falling for Hilbert's Paradox.

The sets in question are not /all/ dynamically/statically typed 
programs, they are all dynamically/statically typed programs that fit 
any item in the set of specifications in existence. Which is a very 
finite set.

> Also, while I don't know a proof, I'm pretty sure that type inferencing
> can do addition (and theorem proving) so is equal in power to
> programming.

Nope. It depends on the type system used: some are decidable, some are 
undecidable, and for some, decidability is unknown.

Actually, for decidable type inference systems, there's also the 
distinction between exponential, polynomial, O (N log N), and linear 
behaviour; for some systems, the worst-case behaviour is unknown but 
benevolent in practice.

The vast majority of practical programming languages use a type 
inference system where the behavior is known to be O (N log N) or better :-)
(meaning that the other type systems and associated inference algorithms 
are research subjects and/or research tools)

Regards,
Jo