Python from Wise Guy's Viewpoint

[Dirk Thierbach]

prunesquallor at comcast.net wrote:
> Dirk Thierbach <dthierbach at gmx.de> writes:

> As I mentioned earlier in this thread, the two things I object to in a
> static type system are these:
> 
>    1)  The rejection of code I know to be useful, yet the system is
>        unable to prove correct.
> 
>    2)  The requirement that I decorate my program with type
>        information to give the type checker hints to enable it 
>        to check things that are, to me, obviously correct.

Yes. I have also said it earlier, but (1) is nearly never going to
happen (if you substitute "correct" with "type correct", and for a
suitable definition of useful), and you don't have to do (2) if there
is type inference.

> Being unable to prove code correct is the same thing as being able to
> prove it incorrect.  This makes three classes of code:
> 
>  1) provably type safe for all inputs
>  2) provably erroneous for all inputs
>  3) neither of the above
>
> Both dynamic and static type systems behave the same way for classes 1
> and 2 except that static systems reject the code in section 2 upon
> compilation while dynamic systems reject it upon execution.  It is
> section 3 that is under debate.

> Those of us that are suspicious of static typing believe that there
> are a large enough number of class 3 programs that they will be
> regularly or frequently encountered. 

Yep. The static typers believe (from experience) that there is a very
small number of class 3 programs, and usually all programs you
normally write fall into class 1. They also know that this is not true
for all static type systems. For languages with a lousy static type
system, there is a large number of class 3 programs, where you have to
cheat to convince the type checker that they are really type safe. The
static typers also believe that with a good static type system, all
useful class 3 programs can be changed just a little bit so they fall
into class 1. In this process, they will become better in almost all
cases (for a suitable definition of "better"). 

> We believe that a large number of these class 3 programs will have
> inputs that cannot be decided by a static type checker but are
> nonetheless `obviously' correct.  (By obvious I mean fairly apparent
> with perhaps a little thought, but certainly nothing so convoluted
> as to require serious reasoning.)

Why do you believe this? A HM type checker doesn't do anything but
automate this "obvious" reasoning (in a restricted field), and points
out any errors you might have made (after all, humans make errors).

> Static type check aficionados seem to believe that the number of class
> 3 programs is vanishingly small and they are encountered rarely.  They
> appear to believe that any program that is `obviously' correct can be
> shown to be correct by a static type checking system.  Conversely,
> they seem to believe that programs that a static type checker find
> undecidable will be extraordinarily convoluted and contrived, or
> simply useless curiosities.

Yes.

> No one has offered any empirical evidence one way or another, but the
> static type people have said `if class 3 programs are so ubiquitous,
> then it should be easy to demonstrate one'.  I'll buy that.  Some of
> the people in here have offered programs that take user input as an
> example.  No sane person claims to read the future, so any statically
> typed check program would have to perform a runtime check.

Yes, and that's what it does. No problem. 

> I (and Don Geddis) happen to believe that there are a huge number of
> perfectly normal, boring, pedestrian programs that will stymie a
> static type checker.  I've been offering a few that I hope are small
> enough to illustrate the problem and not so contrived as to fall into
> the `pointless' class.
> 
> The first program I wrote (a CPS lookup routine) generally confuses
> wimp-ass static type checking like in Java.
> 
> Stephan Bevan showed that SML/NJ had no problem showing it was type
> safe without giving a single type declaration.  I find this to be
> very cool.

Good.

> I offered my `black hole' program and got these responses:
[...]
> Will this the response for any program that does, in fact, fool a
> number of static type checkers?

No. You have also been shown that it can check statically both in
Haskell and OCaml. (I cannot think of any way to make it pass
in C++ or Java, but that's to be expected.)

> This appears to be getting very close to arguing that static type
> checkers never reject useful programs because, by definition, a
> program rejected by a static type checker is useless.

It may not be useless, but you will definitely need to think about
it. And if it is useful, in nearly all cases you can make a little
change or express it a little differently, and it will check.

> Another one was a CPS routine that traverses two trees in a lazy
> manner and determins if they have the same fringe.  The point was not
> to find out if this could be done in SML or Haskell.  I know it can.
> The point was to find out if the static type checker could determine
> the type safety of the program.
> There is a deliberate reason I did not create a `lazy cons'
> abstraction.  I wanted to see if the type checker, with no help
> whatsover, could determine that the type of the lambda abstractions
> that are *implementing* the lazy consing.

See below for "lazy cons".

> Re-writing the program in C++ with huge amounts of type decorations
> and eliminating the lambdas by introducing parameterized classes does
> not demonstrate the power of static type checking.

No, it doesn't. That was just Brian saying "it's so easy, I'll
do it the hard way and demonstrate that it can even be done with
a lousy static type system as in C++".

> Re-writing the program in a lazy language also does nothing to
> demonstrate the power of static type checking. 

May I suggest that you try it yourself? It might be a good way to
get some experience with OCaml, though for a beginner it might take
some time to get used to the syntax etc. Pure lambda terms are the
same in every functional language, after all. 

The only issue is that one should use datatypes for recursive
structures, i.e. one would normally use a 'lazy cons' abstraction
(which would be the natural thing to do anyway). In OCaml, you can get
around this with -rectypes (someone has already demonstrated how to do
lazy lists in this way). In Haskell you would need them, but since
Haskell is already lazy, that's probably not the point.

So yes, for recursive types you need to give the type checker "a
little hint", if you want to put it that way. But that's done on
purpose, because it is the natural way to do it, and it is note done
because it would be impossible to statically check such terms.

So if you are extremely picky, and if you refuse to do the "lazy cons"
initially and consider command line options cheating, that's one of
the programs of class 3 that can be put into class 1 by making a
little change, where this change turns out to make your program better
to understand in the first place. Is this so bad that you want to stay
clear from static typing at any price?

(I bet someone will now comment on that ignoring the "extremely picky"
part :-( .)

- Dirk