Python from Wise Guy's Viewpoint

[Dirk Thierbach]

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

>> Now why does a type system reject a program? Because there's a type
>> mismatch in some branch if the program.

> *or* because the type system was unable to prove that there *isn't* a
> type mismatch in *all* branches.

I am not sure if I read this correctly, but it seems equivalent to what
I say.

  \exists branch. mismatch-in (branch)

should be the same as

  \not \forall branch. \not mismatch-in (branch)

Anyway, I don't understand your point.

(Hindley-Milner typechecking works by traversing the expression tree
in postfix order, matching types on binary application nodes. Typing
fails if and only if such a match fails (ignoring constraints or
similar extensions for the moment) If a match fails, there's a problem
in this branch).

- Dirk