optional static typing for Python

[Kay Schluehr]

On 27 Jan., 23:19, "Russ P." <Russ.Paie... at gmail.com> wrote:
> 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