Python from Wise Guy's Viewpoint

[Andreas Rossberg]

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

You missed one important point here. It is, in fact, trivial to extend 
Hindley-Milner type inference in such a way that it can deal with your 
function. That's what OCaml does when given the -rectypes option. 
However, it is a conscious, deliberate decision not to do so, at least 
not by default!

Why is that? Well, Dirk's quote gives the reason. But let me elaborate.

The design of a type system is by no means canonical. In fact, it is 
based on set of pragmatic decisions and trade-offs. Idealized, you start 
with the trivial type system, which has only one type. Then you refine 
it incrementally by distinguishing certain classes of values through 
introduction of new types and typing rules. Introduction of typing rules 
is based on the following criteria:

- Do they catch a lot of errors?
- Are these errors serious?
- Are they hard to localize otherwise?
- Does the refinement rule out useful constructions?
- Are such constructions common?
- Are they expressible by other means?
- Are the rules intuitive?
- Do they interact nicely with other rules?

And probably more. There are never any definite answers to any of these 
questions. The trade-off depends on many factors, such as the problem 
domain the language is used for. Usually the line is drawn based on 
experience with other languages and known problem domains. In the case 
of arbitrary recursive types, experience with languages that allowed 
them has clearly shown that it caused much more grief than joy.

BTW, almost the same criteria as above apply when you as a programmer 
use the type system as a tool and program it by introducing your own 
types. It can be tremendously useful if you make the right strategic 
decisions. OTOH, especially if you are unexperienced, type abstractions 
might also turn out to be counterproductive.

	- Andreas

-- 
Andreas Rossberg, rossberg at ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
  as kids, we would all be running around in darkened rooms, munching
  magic pills, and listening to repetitive electronic music."
  - Kristian Wilson, Nintendo Inc.