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

[Donn Cave]

However, it's interesting to consider the work that sometimes needs to
go in to specify data structures in some languages - thinking of ML
and friends, as opposed to Java and friends. The campaign for optional
static typing in Python rapidly became bogged down in this matter,
fearing that any resulting specification for type information might
not be the right combination of flexible and powerful to fit in with
the rest of the language, and that's how we really ended up with PEP
3107: make the semantics vague and pretend it has nothing to do with
types, thus avoiding the issue completely.

I missed the campaign for optional static typing, must have been
waged in the developer list. Unless it was not much more than
some on-line musings from GvR a year or two ago. I don't see
how it could ever get anywhere without offending a lot of the
Python crowd, however well designed, so I can see why someone
might try to sneak it past by pretending it has nothing to do
with types. But he didn't -- look at the examples, I think he
rather overstates the potential for static typing applications.

Donn Cave, (e-mail address removed)

 

[George Sakkis]

I missed the campaign for optional static typing, must have been
waged in the developer list. Unless it was not much more than
some on-line musings from GvR a year or two ago. I don't see
how it could ever get anywhere without offending a lot of the
Python crowd, however well designed, so I can see why someone
might try to sneak it past by pretending it has nothing to do
with types. But he didn't -- look at the examples, I think he
rather overstates the potential for static typing applications.

The key point is that this is left to 3rd party libraries; the
language won't know anything more about static typing than it does
now. FWIW, there is already a typechecking module [1] providing a
syntax as friendly as it gets without function annotations. If the
number of its downloads from the Cheeshop is any indication of static
typing's popularity among Pythonistas, I doubt that PEP 3107 will give
significant momentum to any non-standard module anytime soon.

George


[1] http://oakwinter.com/code/typecheck/

 

[Paul Rubin]

Stop here. explicit type signature == declarative static typing !=
unit test.

The user-written signature is not a declaration that informs the
compiler of the type. The compiler still figures out the type by
inference, just as if the signature wasn't there. The user-written
signature is more like an assertion about what type the compiler will
infer. 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.

I have few "surprises" with typing in Python. Very few. Compared to
the flexibility and simplicity gained from a dynamism that couldn't
work with static typing - even using type inference -, I don't see it
a such a wonderful gain. At least in my day to day work.

I'm going to keep an eye out for it in my day-to-day coding but I'm
not so convinced that I'm gaining much from Python's dynamism.
However, that may be a self-fulfilling prophecy since maybe I'm
cultivating a coding style that doesn't use the dynamism, and I could
be doing things differently. I do find since switching to Python 2.5
and using iterators more extensively, I use the class/object features
a lot less. Data that I would have put into instance attributes on
objects that get passed from one function to another, instead become
local variables in functions that get run over sequences, etc.

 

[Paul Rubin]

Wow, you really take non-pollution of the namespace seriously. I agree
it's a wart, but it's one I have happily worked around since day one.

Well, the obvious workaround is just say "list(<some genexp>)"
instead of [<the same genexp>] so that's what I do.

 

[Steve Holden]

Wow, you really take non-pollution of the namespace seriously. I agree
it's a wart, but it's one I have happily worked around since day one.

Well, the obvious workaround is just say "list(<some genexp>)"
instead of [<the same genexp>] so that's what I do.

I think I'll start calling you Captain Sensible. But you are right, it
does avoid that extra little potential for errors.

regards
Steve
--
Steve Holden +1 571 484 6266 +1 800 494 3119
Holden Web LLC/Ltd http://www.holdenweb.com
Skype: holdenweb http://del.icio.us/steve.holden
--------------- Asciimercial ------------------
Get on the web: Blog, lens and tag the Internet
Many services currently offer free registration
----------- Thank You for Reading -------------

 

[sturlamolden]

Reading [1], I wonder: why isn't the compiler making better
use of (purely optional) type labeling? Why not make a compiler
directive so that

a) it will check the types of all my arguments and return
values,

If that is what you want, you can get typechecking using a simple
function decorator:

def typechecked(func):
types = func.func_defaults
def decorator(*args):
if len(args) != len(types):
raise TypeError, 'Wrong number or arguments, expected %d
got %d' % (len(types),len(args))
for a,t in zip(args,types):
if type(t) == type:
if type(a) is not t:
raise TypeError, 'Expected ' + str(t) + ' got ' +
str(type(a))
else:
if type(a) is not type(t):
raise TypeError, 'Expected ' + str(type(t)) + '
got ' + str(type(a))
return func(*args)
return decorator


Now code like this:

@typechecked
def foobar(a = int, b = float, c = tuple):
return None

or

@typechecked
def foobar(a = int, b = float, c = 1.0):
return None

Your calls to foobar will be typechecked (at runtime, not statically),
and a TypeError exception thrown if your calling types were
incorrect.


Regards,

Sturla Molden

 

[Steven D'Aprano]

Python even leaks the index variable of list comprehensions (I've
mostly stopped using them because of this), though that's a
recognized wart and is due to be fixed.

Wow, you really take non-pollution of the namespace seriously. I agree
it's a wart, but it's one I have happily worked around since day one.

Well, the obvious workaround is just say "list(<some genexp>)"
instead of [<the same genexp>] so that's what I do.

I think I'll start calling you Captain Sensible. But you are right, it
does avoid that extra little potential for errors.

I'd be thinking it should be Captain Paranoid. Why is list comp leakage
a worse problem than, well, having local variables in the first place?

def foo(x):
y = something_or_other(x+1)
z = do_something_else(y) + another_thing(y)
# Oh noes!!! y still exists!!1!11!! What to do????
return ("foo", y) # OMG I meant to say z!!!


If your function has got so many lines of code, and so many variables that
this becomes a source of errors, your function should be refactored into
smaller functions.

As far as I can see, the only difference is that the list comp variable
isn't explicitly created with a statement of the form "name = value". Why
is that a problem?

 

[Paul Rubin]

As far as I can see, the only difference is that the list comp variable
isn't explicitly created with a statement of the form "name = value". Why
is that a problem?

I don't know that listcomp vars are worse problem than other vars;
however there is an easy workaround for the listcomp vars so I use it.
If there was a way to restrict the scope of other local vars (I gave
examples from other languages of how this can be done), I'd use that too.

 

[Steve Holden]

I don't know that listcomp vars are worse problem than other vars;
however there is an easy workaround for the listcomp vars so I use it.
If there was a way to restrict the scope of other local vars (I gave
examples from other languages of how this can be done), I'd use that too.

Maybe we just have different styles, and I naturally tend to write in
smaller scopes than you do.

regards
Steve
--
Steve Holden +1 571 484 6266 +1 800 494 3119
Holden Web LLC/Ltd http://www.holdenweb.com
Skype: holdenweb http://del.icio.us/steve.holden
--------------- Asciimercial ------------------
Get on the web: Blog, lens and tag the Internet
Many services currently offer free registration
----------- Thank You for Reading -------------

 

[Paul Rubin]

Maybe we just have different styles, and I naturally tend to write in
smaller scopes than you do.

It's easy to make errors even in very small scopes.

 

[Paul Rubin]

Well, yes, runtime errors occur - in statically typed languages as
well. That's essentially the halting-problem.

Well, no, it's quite possible for a language to reject every program
that has any possibility of throwing a runtime type error. The
halting problem implies that no algorithm can tell EXACTLY which
programs throw errors and which do not. So the language cannot accept
all programs that are free of runtime type errors and reject all
programs that definitely have runtime type errors, with no uncertain
cases. But it's fine for a language to reject uncertain cases and
accept only those which it can rigorously demonstrate have no type
errors.

 

[John Nagle]

Well, no, it's quite possible for a language to reject every program
that has any possibility of throwing a runtime type error. The
halting problem implies that no algorithm can tell EXACTLY which
programs throw errors and which do not. So the language cannot accept
all programs that are free of runtime type errors and reject all
programs that definitely have runtime type errors, with no uncertain
cases. But it's fine for a language to reject uncertain cases and
accept only those which it can rigorously demonstrate have no type
errors.

That's correct. Speaking as someone who once implemented an automatic
proof of correctness system (here's the manual:
http://www.animats.com/papers/verifier/verifiermanual.pdf), the halting
problem isn't an issue. If you write a program for which halting is
undecidable, the program is basically broken.

The way you prove loop termination in the real world is to define
some integer value (you can also use tuples like (1,2,1,3), like
paragraph numbers) that gets smaller each time you go through the
loop, but never goes negative.

Most type issues can be resolved at compile time if you can
see the whole program.

John Nagle

 

[John Nagle]

Well, no, it's quite possible for a language to reject every program
that has any possibility of throwing a runtime type error. The
halting problem implies that no algorithm can tell EXACTLY which
programs throw errors and which do not. So the language cannot accept
all programs that are free of runtime type errors and reject all
programs that definitely have runtime type errors, with no uncertain
cases. But it's fine for a language to reject uncertain cases and
accept only those which it can rigorously demonstrate have no type
errors.

Also, if you're really into this, read this DEC SRL report on
Extended Static Checking for Java, a system from the 1990s.

ftp://gatekeeper.research.compaq.com/pub/DEC/SRC/research-reports/SRC-159.pdf

They were doing great work until Compaq bought DEC and killed off research.

The follow up to that is Microsoft's Spec# effort, which is program
verification for C#. See

http://research.microsoft.com/specsharp/

They have some of the same people, and some of the same code, as the
DEC effort.

Back when I was working on this, we only had a 1 MIPS VAX, and theorem
proving was slow. That's much less of a problem now.

John Nagle

 

[Bruno Desthuilliers]

Paul Rubin a écrit :

The user-written signature is not a declaration that informs the
compiler of the type. The compiler still figures out the type by
inference, just as if the signature wasn't there. The user-written
signature is more like an assertion about what type the compiler will
infer. 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 going to keep an eye out for it in my day-to-day coding but I'm
not so convinced that I'm gaining much from Python's dynamism.

I sure do.

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.

and I could
be doing things differently. I do find since switching to Python 2.5
and using iterators more extensively, I use the class/object features
a lot less. Data that I would have put into instance attributes on
objects that get passed from one function to another, instead become
local variables in functions that get run over sequences, etc.

Dynamism is more than simply adding "cargo" attributes to objects.

 

[Paul Rubin]

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.

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

 

[Diez B. Roggisch]

Well, no, it's quite possible for a language to reject every program
that has any possibility of throwing a runtime type error. The
halting problem implies that no algorithm can tell EXACTLY which
programs throw errors and which do not. So the language cannot accept
all programs that are free of runtime type errors and reject all
programs that definitely have runtime type errors, with no uncertain
cases. But it's fine for a language to reject uncertain cases and
accept only those which it can rigorously demonstrate have no type
errors.

Sure. But which class of programs are decidable? There's lot's of
research going on with model checking and the like. But AFAIK, the
consensus is that the very moment you allow recursive types, the
type-checking is either incomplete, or possibly non-deterministic. Which
makes then the compiler hang.

Diez

 

[Paul Rubin]

Sure. But which class of programs are decidable? There's lot's of
research going on with model checking and the like. But AFAIK, the
consensus is that the very moment you allow recursive types, the
type-checking is either incomplete, or possibly
non-deterministic. Which makes then the compiler hang.

Type checking is already undecidable in many mainstream languages
including C++. Nonetheless people manage to use those languages.

 

[Bruno Desthuilliers]

Paul Rubin a écrit :

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.

I was mostly thinking of inputs, but it's the same thing for outputs -
in most cases the concrete "type" (=> class) of the object returned by a
function is no more significant than the concrete type(s) of it's
input(s). What is important is that these objects supports the
(implicit) protocols expected by either the function itself (for inputs)
or the caller (for output(s)). And FWIW, in Python, it's not unusual for
a function or method to be able to return objects of any type - cf the
dict.get(key, default=None) method.

(snip)

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.

While my knowledge of Lisp is somewhat limited - I played with Common
Lisp and Scheme (and Emacs Lisp) but never seriously used any Lisp
dialect - it also had some influence on my coding style. But Python's
support for "hi-level" programming - including the restricted support
for functional approach - mostly comes from it's object model, and I
prefer to take advantage of this object model instead of trying to write
Lisp (or Haskell or whatever other FPL) in Python. A good example could
be partial application - which in Python is better implemented as a
class than using closures.

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.

Indeed. But this doesn't mean you should not use the rope at all -
specially when it happens to be the RightThing(tm) to do. Compare an old
framework like Zope 2.x, and new ones (internally) making heavy use of
metaclasses, descriptors etc, and you may find out that these features
not only greatly help wrt/ both robustness (less boilerplate) and
readability (less boilerplate), but also tend to encourage a more
declarative style (.

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:

I have too few problems with type errors to feel a need for more "type
safety" than what Python actually provides, and I don't see the point of
adding arbitrary restrictions. What's appropriate for language X is not
necessarily appropriate for language Y, and I know where to find smart
statically typed languages if and when I do need them.

 

[Donn Cave]

Someday we will look at "variables" like we look at goto.

Maybe we just have different styles, and I naturally tend to write in
smaller scopes than you do.

I've wondered if programmers might differ a lot in how much they
dread errors, or how they react to different kinds of errors.
For example, do you feel a pang of remorse when your program
dies with a traceback - I mean, what a horrible way to die?
Do you resent the compiler's reprimands about your code errors,
or nagging about warnings? Maybe the language implementation's
job has as much to do with working around our feelings as anything
else.

Donn Cave, (e-mail address removed)

 

[John Nagle]

I've wondered if programmers might differ a lot in how much they
dread errors, or how they react to different kinds of errors.
For example, do you feel a pang of remorse when your program
dies with a traceback - I mean, what a horrible way to die?
Do you resent the compiler's reprimands about your code errors,
or nagging about warnings? Maybe the language implementation's
job has as much to do with working around our feelings as anything
else.

That's worth thinking about.

I've worked in big mainframe shops, where an operating system
crash caused everything to suddenly freeze, red lights came on all
over the building, and a klaxon sounded. I've worked for aerospace
companies, where one speaks of "defects", not "bugs", and there
are people around whose job involves getting in high performance
aircraft and flying with the software written there. I've worked
with car-sized robot vehicles, ones big enough to injure people.

This gives one a stronger feeling about wanting to eliminate
software defects early.

John Nagle