Python from Wise Guy's Viewpoint

[Lex Spoon]

>>>It sounds unbelievable, but it really works.
>> I believe you.  I have trouble swallowing claims like `It is never
>> wrong, always completes, and the resulting code never has a run-time
>> error.' or `You will never need to run the kind of code it doesn't allow.'
>
> This kind of claim comes is usually just a misunderstanding.
> For example, the above claim indeed holds for HM typing - for the
> right definitions of "never wrong" and "never has an error".
>
> HM typing "is never wrong and never has a run-time error" in the
> following sense: the algorithm will never allow an ill-typed program
> to pass, and there will never be a type error at run-time. However,
> people tend to overlook the "type" bit in the "type error" term, at
> which point the discussion quickly degenerates into discourses of
> general correctness.


It is misleading to make this claim without a lot of qualification.
It requires careful, technical definitions of "type" and "type error"
that are different from what an unprepared audience will expect.


For example, it is not considered a type error if you get the wrong
branch of a datatype.  So if you define:

   datatype sexp = Atom of string | Cons of (sexp, sexp)
  
   fun car (Cons (a,b)) = a

then the following would not be considered a "type error" :

   car (Atom "hello")



To add to the situation, HM flags extra errors, too, that many people
would not consider "type errors" but which are for HM's purposes.  For
example, it is considered a type error if two branches of an "if" do
not match, even if one branch is impossible or if the later code can
remember which branch was followed.  For example:

   val myint : int  = 
     if   true
     then 0
     else "hello"


or more interestingly:

   val (tag, thingie) =
     if (whatever)
     then  (0, 1)
     else  (1, 1.0)

   val myotherstuff = 
     if tag = 0
     then (tofloat thingie) + 1.5
     else thingie + 1.5


In common parlance, as opposed to the formal definitions of "type
error", HM both overlooks some type errors and adds some others.  It
is extremely misleading to claim, in a non-technical discussion, that
HM rejects precisely those programs that have a type error.  The
statement is actually false if you use the expected meanings of "type
error" and "type".


All this said, I agree that HM type inference is a beautiful thing and
that it has significant benefits.  But the benefit of removing type
errors is a red herring--both in practice and, as described in this
post, in theory as well.

-Lex