Python from Wise Guy's Viewpoint

[Joe Marshall]

"Andrew Dalke" <adalke at mindspring.com> writes:

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

They aren't the same size if you limit the length of the program.  This
is a reasonable restriction if you are interested in programs that might
be realizable within your lifetime.

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

Yes, this is true.  But it is also the case that a powerful enough
static type checker cannot be proven to halt or produce an answer in a
time less than that required to run the program being checked.  It
makes little difference if the type checker produces the answer or the
program produces the answer if they both take about the same time to
run.  Of course, it is generally more difficult to program in the type
metalanguage than in the target language.