PEP 3107 and stronger typing (note: probably a newbie question)

[Paul Rubin]

Bruno Desthuilliers <bruno.42.desthuilliers at wtf.websiteburo.oops.com> writes:
> > If the assertion is wrong, the compiler signals an error.  In
> > that sense it's like a unit test; it makes sure the function does what
> > the user expects.
> 
> It still boils down to the same problem : possibly valid types are
> rejected based on a declaration.

I'm not sure what you mean.  If the programmer intended for the
function to compute an integer, then it's invalid for the function to
return (say) a string, whether there is a static typecheck or not.
The type signature just makes sure the function works as intended, at
least as regards its return type.

If you mean that the programmer might have valid reasons to return a
mix of types dynamically and static languages get in the way of that,
well sure that's true, though I suspect that polymorphism and
algebraic types can handle most of these cases.

> > However, that may be a self-fulfilling prophecy since maybe I'm
> > cultivating a coding style that doesn't use the dynamism,
> 
> Perhaps is this coding style not making the best use of Python's
> features ? To me, it sounds like doing procedural programming in OCaml -
> it's of course possible, but probably not the best way to use the language.

This is in principle possible, though I feel like I'm coding more
effectively since gravitating to this style.  Anton van Straaten (a
dynamic typing proponent) wrote of static checks
(http://lambda-the-ultimate.org/node/2216#comment-31954):

    In most cases, the correctness proof itself is not the most important
    advantage of static checking of a program. Rather, it's the type
    discipline that must be followed in order to achieve that correctness
    proof. The final proof is like the certificate you get when you
    graduate from college: it's not that important by itself, but to have
    obtained it you must have done a lot of work, at least some of which
    is important and necessary. You can do the work without getting the
    certificate, but many people don't, and in the programming case they
    may pay a price for that in terms of programs with poor type
    discipline, which can have consequences for reasoning and the
    "ilities".

I coded a fair amount of Lisp before starting with Python though, so
even before, I tended to code Python in a Lisp-like style, ignoring
Python's more dynamic features such as metaclasses.

I'd also compare the situation with Forth, where functions can consume
and insert arbitrary numbers of values to the stack, but programmers
in practice maintain careful stack discipline (making sure to pop and
push a constant number of values, and documenting the meaning of each
one) in order to avoid going crazy.  Just because the language offers
you rope, doesn't mean you can't decline to hang yourself with it.

Finally, this article about "gradual typing" (you can write your code
dynamically and then later add static annotations resulting in type
safety) might be of interest:

  http://lambda-the-ultimate.org/node/1707