optional static typing for Python

[Bruno Desthuilliers]

Russ P. a écrit :

On Jan 27, 5:03 pm, Paddy


Yes, but for safety-critical software you usually want the simplest
possible solution. The last think you want is an unnecessarily "fancy"
design. Unless there is a darn good reason to write a "non-static"
program, you just don't do it.

You might want to check into what the FAA allows in "flight-critical"
code, for example. I am certainly not an expert in that area, but I've
had a passing exposure to it. My understanding is that every possible
branch of the code must be fully and meticulously analyzed and
verified. Hence, the dynamic dispatching of ordinary object-oriented
code is either prohibited or severely frowned upon.

Then Python is definitively out, so this whole thread is pointless.

 

[Paul Rubin]

You might want to check into what the FAA allows in "flight-critical"
code, for example. I am certainly not an expert in that area, but I've
had a passing exposure to it. My understanding is that every possible
branch of the code must be fully and meticulously analyzed and
verified. Hence, the dynamic dispatching of ordinary object-oriented
code is either prohibited or severely frowned upon.

This would also seem to impact higher-order functions, which are
prominent in fancy verification systems based on extracting code from
constructive theorem provers. I know those things are used in some
sensitive security applications. I wonder what the aerospace
community thinks of that area.

 

[Russ P.]

Russ P. a écrit :






Then Python is definitively out, so this whole thread is pointless.

Yes, Python as it stands now is "definitely out" as the ultimate
implementation language for flight-critical software. That's
essentially a no-brainer. But it can certainly be useful as a
prototyping language for R&D.

The question then arises as to how to best make use of the prototype.
Do you throw away the code and start from scratch? That doesn't seem
wise to me. But maybe that's because I have some idea of how much
effort can go into developing a good prototype.

If Python could be automatically converted to Ada or Java, that could
potentially be used as a baseline for actual operational software.
That would capture the algorithmic details more reliably than recoding
from scratch by hand. But such an automatic conversion is not feasible
without explicit typing.

And speaking of "pointless," ... I just wasted a significant amount of
time replying to a pointless post. Oh, well.

 

[Russ P.]

Russ P. a écrit :> A while back I came across a tentative proposal from way back in 2000

Lord have mercy(tm).

What is that supposed to mean?

Oh, I almost forgot. I'm supposed to sit here and be polite while
clueless dolts make wise cracks. Sorry, but I haven't yet mastered
that level of self-control.

I would just like to thank you for reminding me about what losers hang
out perpetually on sites like this one, thinking they are in some kind
of real "community." Being reminded of that will help prevent me from
becoming such a loser myself. No, I didn't say that all the "regulars"
here are losers, but you most certainly are.

Do you have a job? How about a life? Have you ever been "with" a
woman? How in the world is it that every time I come to this site, I
see your sorry ass hanging around yet again? I can't even imagine how
"pointless" your life must be if you have that much time to spend
"hanging around" on comp.lang.python -- and being an a--hole to boot.

Yeah, Lord have mercy -- on losers like you.

And thanks for reminding me to quit wasting so much time here. I've
been doing way too much of that lately.

 

[cokofreedom]

What is that supposed to mean?

Oh, I almost forgot. I'm supposed to sit here and be polite while
clueless dolts make wise cracks. Sorry, but I haven't yet mastered
that level of self-control.

I would just like to thank you for reminding me about what losers hang
out perpetually on sites like this one, thinking they are in some kind
of real "community." Being reminded of that will help prevent me from
becoming such a loser myself. No, I didn't say that all the "regulars"
here are losers, but you most certainly are.

Do you have a job? How about a life? Have you ever been "with" a
woman? How in the world is it that every time I come to this site, I
see your sorry ass hanging around yet again? I can't even imagine how
"pointless" your life must be if you have that much time to spend
"hanging around" on comp.lang.python -- and being an a--hole to boot.

Yeah, Lord have mercy -- on losers like you.

And thanks for reminding me to quit wasting so much time here. I've
been doing way too much of that lately.

Why is it everyone has to resort to name calling and instantly being
offended by everyone. If you don't think he reply has merit, then
either simply ask him what he meant or ignore the post altogether.
Your reply just flames the issue.

I never get the reason why people feel the need to insult someone they
feel has insulted them. That somehow by the re-doing the act they will
solve the issue? Just move on.

 

[Torsten Bronger]

Hallöchen!

What is that supposed to mean?

So you haven't understood him. Then why is this rant following?

Anyway, I can only speak for myself: I have the concern that any
(albeit optional) declaring of types in Python leads to people
thinking that their code is more valuable with such declarations.
Mostly you know which type is to be expected after all.

As a result, you see such declarations everywhere, whether helpful
or not. Maybe eventually tools such as pylint will even give a
percentage how many parameters are annotated, and people try to
maximize this value. Ugh.

Then, Python is not as useful anymore because readability falls
drastically. Moreover, there is a Fortran saying: "One person's
constant is another person's variable." The same applies to types
in Python.

Pythons is one way, Ada another way; there is no silver bullet.

Tschö,
Torsten.

 

[Diez B. Roggisch]

If Python could be automatically converted to Ada or Java, that could

potentially be used as a baseline for actual operational software.
That would capture the algorithmic details more reliably than recoding
from scratch by hand. But such an automatic conversion is not feasible
without explicit typing.

If python could be automatically converted to ADA or Java, it wouldn't be
python. The fundamental difference IS the lack of static type annotations.
The problem is that people often confuse type inference with dynamic
typing, because it looks similar - but it isn't the same. All typeinference
does is to take an expression like this:

a = 10 * 100

and place type-variables on it, like this:

a:t_0 = 10:int * 100:int

Actually, the multiplication also gets annotated, like this:

a:t_0 = *(10:int, 100:int):t_1

Then the unknown type variables are inferred - it is known (and that is an
important property: ALL FUNCTIONS ARE KNOWN AT THIS POINT) that there
exists a multiplication function that has this signature:

_ * _ : [int, int] -> int

so t_1 can be inferred to be int, thus t_0 can be inferred to be int as
well.

But the key-point is: each and every function declaration is and has to be
fully statically typed. And all of them have to be known at compile-time!!
And of course this extends to classes or interfaces and such.

There are some nice tricks like generic types that themselves containt
type-variables in their declaration, so that you can declcare e.g. map,
reduce, filter and so forth in generic ways. But they are _fully_ type
annotated.

And the "normal" (Henly/Millner) type inference fails to produce correct
results in cases like this:

def foo(arg):
if arg > 10:
return 100
else:
return "n/a"

Which is perfectly legal and sometimes useful in python. Yes, there is
dependent typing, but this also goes only so far.

Additionally, it can be shown that type-inferencing becomes
non-deterministic or even unsolvable in the very moment you start
introducing recursive types - so, away with lists, arrays, trees and so
forth. Which of course also means that the statically typed languages will
produce errors, unless you restrict them heavily with respect to dynamic
memory allocation and so forth (that restricted ADA variant sometimes
popping up in discussions about this is one such case)

bottom-line: type-inference doesn't do magic, fully staticly annotated
languages still fail, and efforts like shedskin are interesting but will
never grow to a full-fledged python. And adding static type-declarations to
python will make it NotPython, a totally different language.

Diez

 

[Bruno Desthuilliers]

Russ P. a écrit :

What is that supposed to mean?

That I definitively don't agree with you on this point and would prefer
that statically-typed languages proponants (and specially those advocate
declarative typing) leave Python alone.

Oh, I almost forgot. I'm supposed to sit here and be polite while
clueless dolts make wise cracks. Sorry, but I haven't yet mastered
that level of self-control.

I would just like to thank you for reminding me about what losers hang
out perpetually on sites like this one, thinking they are in some kind
of real "community." Being reminded of that will help prevent me from
becoming such a loser myself. No, I didn't say that all the "regulars"
here are losers, but you most certainly are.

Do you have a job?
Yes.

How about a life?
Idem.

Have you ever been "with" a
woman?

I'm married and have kids, and we're pretty happy, thanks.

How in the world is it that every time I come to this site, I
see your sorry ass hanging around yet again? I can't even imagine how
"pointless" your life must be if you have that much time to spend
"hanging around" on comp.lang.python -- and being an a--hole to boot.

Yeah, Lord have mercy -- on losers like you.

And thanks for reminding me to quit wasting so much time here. I've
been doing way too much of that lately.

How does it come that you having nothing better to do than insulting
peoples that happen to disagree with you ?

 

[Kay Schluehr]

A while back I came across a tentative proposal from way back in 2000
for optional static typing in Python:

http://www.python.org/~guido/static-typing

Two motivations were given:

-- faster code
-- better compile-time error detection

I'd like to suggest a third, which could help extend Python into the
safety-critical domain:

-- facilitates automated source-code analysis

There has been much heated debate in the past about whether Python is
appropriate for safety-critical software. Some argue that, with
thorough testing, Python code can be as reliable as code in any
language. Well, maybe. But then, a famous computer scientist once
remarked that,

"Program testing can be used to show the presence of bugs, but never
to show their absence!" --Edsger Dijkstra

The next step beyond extensive testing is automated, "static" analysis
of source-code ("static" in the sense of analyzing it without actually
running it). For example, Spark Ada is a subset of Ada with
programming by contract, and in some cases it can formally prove the
correctness of a program by static analysis.

Then there is Java Pathfinder (http://javapathfinder.sourceforge.net),
an "explicit state software model checker." The developers of JPF
wanted
to use it on a prototype safety-critical application that I wrote in
Python, but JPF only works on Java code. We considered somehow using
Jython and Jythonc, but neither did the trick. So they ended up having
someone manually convert my Python code to Java! (The problem is that
my code was still in flux, and the Java and Python versions have now
diverged.)

In any case, optional static typing in Python would help tremendously
here. The hardest part of automated conversion of Python to a
statically typed language is the problem of type inference. If the
types are explicitly declared, that problem obviously goes away.
Explicit typing would also greatly facilitate the development of a
"Python Pathfinder," so the conversion would perhaps not even be
necessary in the first place.

Note also that, while "static" type checking would be ideal,
"explicit" typing would be a major step in the right direction and
would probably be much easier to implement. That is, provide a syntax
to explicitly declare types, then just check them at run time. A
relatively simple pre-processor could be implemented to convert the
explicit type declarations into "isinstance" checks or some such
thing. (A pre-processor command-line argument could be provided to
disable the type checks for more efficient production runs if
desired.)

I noticed that Guido has expressed further interest in static typing
three or four years ago on his blog. Does anyone know the current
status of this project? Thanks.

It has been withdrawn in its original version. What's left is
annotation syntax and the __annotation__ dict ( I don't know what the
latter is good for but maybe some purpose emerges once a complete
signature object is provided? ). So there has not been much work spent
on hybrid type systems, static analysis and type directed native
compilation.

I did some work on type feedback and created a Python dialect called
TPython a while ago based on Python 3.0 but supporting more syntax to
add also local type annotations and an 'A of T' construct for type
parametricity. The main purpose of TPython was to provide an interface
for 3rd party tools used for refactoring, type checking, compilation,
documentation etc. without separating annotations from Python code but
build them in place.

This project is unpublished and on hold because it is part of
EasyExtend 2.0 and I reworked EE to incorporate a brand new parser
generator called Trail that involved quite some research from my side.
EasyExtend 3 is intended to be released in Q2.

Regards

 

[John Nagle]

Note that annotations do not provide explicit typing, AFAIK:

def f(x:int) -> int: return x*2

is stricly equivalent to

def f(x): return x*2
f.__annotations__ = {'x':int, 'return':int}

You still need to write a type-checking wrapper.

Unenforced static typing is somewhat pointless. If that
goes in, it should be enforced by implementations. Otherwise,
maintenance programmers can't trust the type information they see.

Enforced, it makes it possible to start getting serious about
optimizing compilers for Python, like Shed Skin. Shed Skin
can usually figure out typing within a module, but across module
boundaries, some help is needed if you want to push optimization from
run time to compile time.

John Nagle

 

[Boris Borcic]

Wish you'd opted out of typing all that static.

BB

Russ P. wrote:
(...)

 

[Marc 'BlackJack' Rintsch]

Unenforced static typing is somewhat pointless. If that
goes in, it should be enforced by implementations.

Luckily we don't get static typing. We get annotations which *can* be
used for type hints, checked by additional code. Can be used for other
things as well.

Ciao,
Marc 'BlackJack' Rintsch

 

[Arnaud Delobelle]

Arnaud Delobelle wrote: [...]

Note that annotations do not provide explicit typing, AFAIK:

def f(x:int) -> int: return x*2

is stricly equivalent to

def f(x): return x*2
f.__annotations__ = {'x':int, 'return':int}

You still need to write a type-checking wrapper.

    Unenforced static typing is somewhat pointless.  If that
goes in, it should be enforced by implementations.  Otherwise,
maintenance programmers can't trust the type information they see.

(As discussed earlier, there is no static typing in Python, there can
only be runtime type-checking or, as someone called it, "explicit
typing")
I think the idea is to let the user decide how to enforce type-
checking, not the language. I suppose if in a few years a way to do
it emerges that is "the best", then it'll make its way into the
standard library...

 

[Ben Finney]

I would just like to thank you for reminding me about what losers
hang out perpetually on sites like this one, thinking they are in
some kind of real "community." Being reminded of that will help
prevent me from becoming such a loser myself. No, I didn't say that
all the "regulars" here are losers, but you most certainly are.

We're a community largely because we don't tolerate this level of
content-free insult. Please find a different forum for this stuff.

 

[Chris Mellon]

Unenforced static typing is somewhat pointless. If that
goes in, it should be enforced by implementations. Otherwise,
maintenance programmers can't trust the type information they see.

Enforced, it makes it possible to start getting serious about
optimizing compilers for Python, like Shed Skin. Shed Skin
can usually figure out typing within a module, but across module
boundaries, some help is needed if you want to push optimization from
run time to compile time.

Given the difficulty of statically analyzing Python, and the
limitations you need to add for either static typing or type inference
to be practical, I think that the real future for faster Python code
is JIT, not static optimizations. Languages which enforce static
typing are, of course, not Python - that's why they have different
names, like Pyrex or ShedSkin or RPython.

I think static Python is pretty much a waste of time, really - if I'm
going to write statically typed code using a traditional C/C++/Java
style type system, I'll use a language designed for it, like D. If I
want *real* strict typing - the kind where you can actually make a
useful inference from the fact that the program is type-correct - I'll
use Haskell or Ocaml. There is a lot of choice out there and there's
no reason to try to make Python into whatever your favorite paradigm
is.

 

[Kay Schluehr]

Given the difficulty of statically analyzing Python, and the
limitations you need to add for either static typing or type inference
to be practical, I think that the real future for faster Python code
is JIT, not static optimizations.

Python has a JIT right now - so why do you think it's Pythons "real
future"?

 

[Wildemar Wildenburger]

Python has a JIT right noYou mean in the Java-sense (outputting native machine code)?

/W

 

[bruno.desthuilliers]

Yes, Python as it stands now is "definitely out" as the ultimate
implementation language for flight-critical software. That's
essentially a no-brainer. But it can certainly be useful as a
prototyping language for R&D.

The question then arises as to how to best make use of the prototype.
Do you throw away the code and start from scratch? That doesn't seem
wise to me. But maybe that's because I have some idea of how much
effort can go into developing a good prototype.

If Python could be automatically converted to Ada or Java, that could
potentially be used as a baseline for actual operational software.
That would capture the algorithmic details more reliably than recoding
from scratch by hand. But such an automatic conversion is not feasible
without explicit typing.

As far as I can tell, this should be possible using type annotations
and some "soft" (ie: coding style guideline) restrictions on the most
dynamic features. This may even be possible without type annotation,
if I refer to the work being done on RPython for Pypy.

This being said, I don't personaly believe that much in "automatic
conversion" from Python to Java or Ada, because a language is not only
made of a syntax and grammar, but also of idioms, and I really doubt
you'll get idiomatic Java or Ada from idiomatic Python - unless your
Python code is written in Javaish (or Ada-ish) idioms, in which case
using Python is IMHO, well, how to say... somewhat pointless ?-)

And speaking of "pointless," ... I just wasted a significant amount of
time replying to a pointless post. Oh, well.

Coming from someone posting here that declarative static typing would
make a better Python just because *he* thinks he have a need for it,
without any consideration for the fact that most people here use
Python because they don't actually want static typing, and without
even realizing that most of what makes Python great for prototyping is
it's dynamism, I do find this use of terms like "pointless" and "waste
of time" *very* amusing. Almost as amusing as this other post where
you so kindly worried about my job and personal life.

 

[Kay Schluehr]

You mean in the Java-sense (outputting native machine code)?

/W

Sure.

http://psyco.sourceforge.net/

 

[Wildemar Wildenburger]

Sure.

http://psyco.sourceforge.net/

Oh, switcheroo!

/W