Python from Wise Guy's Viewpoint

[Dirk Thierbach]

Joe Marshall <jrm at ccs.neu.edu> wrote:
> Dirk Thierbach <dthierbach at gmx.de> writes:
>> It will be successfully type checked, because the static type system
>> does not allow you to express assumptions about value ranges of types.

> I was working on the assumption that the type language *would* allow
> one to express arbitrary types. 

It doesn't. (There are languages with a type languages that do
allow to express arbitrary types, but the consequence is that typing
is no longer decidable at compile-time, so your compilation may
not terminate. For many people, this is not acceptable.)

> Certainly one can create a sufficiently weak static type system that
> terminates under all conditions and produces correct answers within
> the system.

Yes. The trick is that there is a fine line between "too weak" and
"not decidable". As I repeatedly said, it helps to think of the
static type system as a tool that automatically writes tests in
a limited area, but these tests are more powerful than unit tests
because they work on all possible execution paths. But this tool
clearly won't write all the tests you need, so for the rest, you
insert checks or write the unit tests by hand.

> But I surely wouldn't be impressed by a type checker that allowed this
> to pass:

[more stuff with value ranges]

It's not a question whether it will pass or fail. You cannot express 
this in the type language.

Maybe the misunderstanding is that you and others think that a static
type checker must now check everything at compile time that is checked
at runtime with dynamic typing. It doesn't, and in those cases where
it doesn't, you of course write the same tests in a statically typed
language as you do in a dynamically typed language.

But that doesn't mean static typechecking is not useful; it *will*
help you in a lot of cases.

> I think most people here were assuming that passing an integer greater
> than 255 to a routine expecting a single 8-bit byte is a type error,
> and something that could cause a crash.

But that's not how it works. What you can use the static type system
for is to make two different types, say Byte and Integer, and then
write a conversion routine from Integer to Byte that does a range check,
and the type checker will make sure that this conversion routine
is called everywhere where it is necessary. So you can use the type
checker to remind you when you forget that. (That's quite helpful,
because it is easy to forget adding a manual type check.)

(And, BTW, that's quite different from C where the static typechecker
allows you to assign values of different ranges without ever asking
for a range check.)

- Dirk