Python from Wise Guy's Viewpoint

[prunesquallor at comcast.net]

Dirk Thierbach <dthierbach at gmx.de> writes:

> prunesquallor at comcast.net wrote:
>> gt5163b at prism.gatech.edu (Brian McNamara!) writes:
>
>>> This one is so easy, we do it in C++ just for spite.  :)
>>> I'm using the FC++ library as a helper.
>
>> Yuck!  Type declarations *everywhere*.  Where's this famous inference?
>
> You *did* notice that it is C++, which hasn't type inference (and
> a lousy typesystem? :-) So what Brian is saying that this is so easy
> he can even to it with hands tied on his back and standing on his
> head.

I did in fact notice that.  It's *supposed* to be easy.  It's
*supposed* to be something simple and useful.

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.

These are personal preferences, but they are shared by many of my
fellow lisp hackers.  To my knowledge, not one of my fellow lisp
hackers would mind a static type checker that noticed code fragments
that could be proven to never produce anything but an error provided
that said type checker never need hints and is never wrong.  Many lisp
systems already have a weak form of this:  try compiling a program that
invokes CAR on 2 arguments or attempts to use a literal string as a
function.

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.

We can categorize class 3 by partitioning the inputs.  Some inputs
can be shown to always produce a type error, some can be shown to
*never* produce a type error, and some are undecidable.  All the class
3 programs contain inputs in at least two of these partitions.

The question remains over what to do with class 3 programs.  Of course
what we do may depend on how often a class 3 program is encountered,
what the risk might be of running one, and possibly the compile time
cost of detecting one.

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

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.

Some people in the static type check camp are making blanket
statements like:

  Matthias Blume 
     Typical "Gödel" statements tend to be pretty contrived.

  Dirk Thierbach <dthierbach at gmx.de> writes: 
    ...the sane programs that are taken away are in most cases at
    least questionable (they will be mostly of the sort: There is a
    type error in some execution branch, but this branch will never be
    reached)

  Joachim Durchholz <joachim.durchholz at web.de> writes:
    ... given a good type system, there are few if any practial
    programs that would be wrongly rejected.

  Matthias Blume
    `...humans do not write such programs, at least not
     intentionally...' 


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.

But this is shooting fish in a barrel, so I'll give you a pass on it.

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.

I offered my `black hole' program and got these responses:

  Remi Vanicat <vanicat+invalid at labri.fr>
    `I don't see how this function can be useful...'

  Jesse Tov <tov at eecs.harvREMOVEard.edu>
    `we don't need functions with those types.'

  Dirk Thierbach <dthierbach at gmx.de>
    `recursive types are very often a result of a real typing error.'

  "Marshall Spight" <mspight at dnai.com>
    `I don't believe the feature this function illustrates could be
     useful.' 

Will this the response for any program that does, in fact, fool a
number of static type checkers?

  Marshall Spight wrote:
   `I'm trying to see if anyone can come up with a program
    that is small, useful, and not provably typesafe.'

  to which Joachim Durchholz <joachim.durchholz at web.de> replied:
   ``Matthias' and my position is that such a program doesn't exist
     (and cannot even exist)''


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.

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.

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.

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