[Types-sig] Core Python.... (less is more)

[Daniel Wang]

I'm a bit new to the Python community, but being a graduate student stuck in
academia. I was quite amazed to see a community of its own free will wanting
to add static types into their favorite previous untyped language. (No days
of lecturing and subversive homework assignments to brain wash you guys into
thinking static types are useful....)

I'm curious as to what if any interaction there has been between with the
academic community. I've spent quiet a great deal of time studying and
implementing relatively advanced type systems and am just dying to see one
deployed for a "real language" that isn't Java.

Those familiar with Generic Java will know that a lot of work was put in by
some academics to get a design palatable enough for Sun to consider
adopting. Even after all that got put into it, GJ is still "stuck in the
labs". It would be nice to try to replicate a similar kind of interaction
with the Python, with a slightly different outcome. (i.e. where the research
gets set free and used by real people.)

However, full Python seems to present some non-trivial challenges for
existing type systems and is very difficult to discuss. I'm curious if it
is possible to come up with a small subset of Python that has the following
properties...

  1. Is the core part of Python i.e. most if not all other constructs can be
     explained in terms of core features.
  2. Small enough to admit a rigorous formal specification
  3. Large enough to program interesting Python programs 
  4. Small enough to easily hack up toy type checkers and type tools
  5. Large enough so as not to hide the underlying typing difficulties

A nice small core language is quiet easy to a pointed headed type theorist
and say "build me a type system for this". Points 2 and 3 are important for
the type theorists so there's some chance of writing all these things up
and publish it and maybe get tenure. :) (shoving them a Python manual or
even the existing documents at an academic requires the academic spend a lot
of time trying to figure out what's going on... 

Points 4.are 5. important of hacking prototyping and general discussion on
the mailing list. So is anyone interested in formulating "core Python"?

Once you have "core Python" one could take on a a slightly more ambitious
project. One could extend core Python with enough features but still simple
enough to admit a relatively simple static typing system which would be
similar to ML or a safe C with polymorphism. Let's call this language
"systems Python". The next step is to write a translator for "systems Python"
into C, and finally perform the Squeak trick of writing a Python runtime
system in a statically typed variant of Python itself.

From this "systems Python", it then might be easier to slowly added more an
more typing features until the majority if not a very large subset of Python
is finally statically typeable, and efficiently compilable into C.

Reading the existing proposals they all have the feeling of "we're not sure
we've got it right here..." I think the solution to this problem is to start
small and slowly test the design of the static type system. The task of
bootstrapping Python would be a good way to test the design of the type
system, and also more importantly investigate how the static type system
aids compilation.

Even if "systems Python" is a small of Python if it is efficiently
compilable into C. People can at least consider writing extension in this
subset rather than giving up and programming in C when Python gets a bit too
slow. 

So anyone interested in helping figure out what "core Python" and "systems
Python" actually look like... or has someone done this already?

P.S. Turth in advertising disclaimer: This my subversive attempt to see some
of all the research, I've been seeing and doing myself actually get
used... and to push my own hidden agenda so I can convice the world that
"types are cool".