Python from Wise Guy's Viewpoint

[Joachim Durchholz]

prunesquallor at comcast.net wrote:
> 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.

Er... for static type systems, it's just "type-correct". General 
correctness isn't very well-defined and not what current main-stream 
type systems are designed for anyway.

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

I'd agree with these points, and restate that both are addressed by 
Hindley-Milner type systems.

1) Most useful code is type-correct. The code that isn't uses quite 
advanced types, but these are borderline cases like "black-hole" above. 
Besides, I don't know of any borderline case that cannot be written 
using different techniques.

2) Decorating programs with type annotations is an absolute exception. 
The only case where types are declared are those where you define a new 
type (i.e. record types).

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

A HM checker flags some usages as "wrong" that would work in Lisp - 
black-hole is an example.
I'm not sure that such usage serves a good purpose.

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

That's exceedingly weak indeed.
Distinguishing square from nonsquare matrices goes a bit beyond the 
standard usage of HM type systems, but it is possible.

> Being unable to prove code correct is the same thing as being able to
> prove it incorrect.

This true for HM typing but not true for inference systems in general. 
But probably you wanted to say something else anyway.

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

Agreed.
Programs in class 2 are rarely encountered and quickly fixed, so I'm not 
sure that this category is very interesting.

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

There's also the question how to decide whether a program is in class 1 
or class 3.

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

This belief is ill-founded. Just take a dynamically-typed program and 
annotate every parameter with all the types that you expect it to take 
on. Exclude possibilities if you hit a contradiction. Get suspicious if, 
for some parameter, there is /no/ type left :-)
You'll find that most programs will type readily.
(HM typing indeed starts with allowing all types for all names, then 
excluding all types that lead to a contradiction somewhere. The actual 
wording of the algorithm is somewhat different, but that's the gist of it.)

 > (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)''

Sorry, you're mixing up topics here - that was about correctness in 
general, not about type correctness (which is a subset of general 
correctness for the vast majority of type systems).

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

That's a misunderstanding, partly due to conflation of correctness and 
type correctness, partly because people using a good static type checker 
don't feel constrained by that type checking because "you just don't do 
that" (similarly to "you just don't do some special things in Lisp", 
like abusing MOP mechanisms etc.)

Regards,
Jo