Python from Wise Guy's Viewpoint

[Dirk Thierbach]

Joe Marshall <jrm at ccs.neu.edu> wrote:
> I have trouble swallowing claims like `It is never wrong, always
> completes, and the resulting code never has a run-time error.'

I can understand this. Fortunately, you don't have to swallow it,
you can verify it for yourself.

A comprehensive book about the lambda calculus should contain the
Hindley-Mindler type inference algorithm. The HM-algorithm is fairly
old, so I don't know if there are any papers on the web that explain
it in detail. Unification of types and the HM-algorithm together are
maybe two pages.

* Termination is easy to verify; the algorithm works by induction on
  the structure of the lambda term.

* For "it never has a runtime error" look at the typing rules of
  the lambda calculus and convince yourself that they express the
  invariant that any function (including "constants", i.e. built-in
  functions) will only be applied to types that match its own
  type signature. Hence, no runtime errors.

  A good book will also contain the proof (or a sketch of it) that
  if the HM-algorithm succeeds, the term in question can indeed by
  typed by the typing rules.

* For the other case (i.e., there is a mismatch during unification; I
  guess that's what you mean by "it is never wrong"), try to assign to
  every variable a value of the type under the current type
  environment, and reduce along every possible reduction path of the
  subterm. One of those reductions will fail with a type error (though
  this reduction may never happen if execution never reaches this part
  of the subterm on the path that the evaluation strategy of your
  language chooses).

  Maybe it's best to do this for a few examples.
  
> or `You will never need to run the kind of code it doesn't allow.'

The last point should show that such a code at least is problematic,
unless you can somehow make sure that the part that contains the
type error is never executed. In that case, this part is useless,
so the code should be probably rewritten. At least I cannot think
of a good reason why you would "need" such kind of code.

- Dirk