Python from Wise Guy's Viewpoint
dthierbach at gmx.de
Sat Oct 25 02:24:09 CEST 2003
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
\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).
More information about the Python-list