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

[Paul Prescod]

Daniel Wang wrote:
> 
> 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....)

Yes, but there is strong agreement in the Python community that static
types need to be entirely optional. 

> 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.

The interest in static types comes in fits and starts (typically after
conferences). We did get some academic interest just before the last
wave died out. So no, we haven't really had much serious academic input
yet.

> 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.)

In my opinion, Generic Java was a lot easier than "static python". I
think that you are familiar with the problems.

> 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...

Your last point makes your approach unique. Traditionally we have talked
about Python subsets specifically chosen to be *easier* to optimize.
Later in your email you seem to be talking about the same thing.

> 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.

Let's be careful here. Any language that is rougly like ML or "safe C"
is not nearly as dynamic as Python. You have to decide whether you are
interested in a very dynamic, but small Python subset or a static Python
subset.

> >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.

If that's possible, it sure isn't easy.

> Reading the existing proposals they all have the feeling of "we're not sure
> we've got it right here..." 

Okay, but consider the difference between the academic's view of "got it
right" and the Python programmers. The acadmic's wants a clean
mathematical abstraction. The Python programmer wants something that
"feels like Python." And we all have different ideas of what feels like
Python....

I think that that is the real problem. We don't all agree on what we
want. There are three major subdivisions, those who want better error
checking (ERR), those who want better performance (OPT) and those who
want better documentation(DOC). Now we can divide those three into six
by differentiating between those who want better ERR and DOC at module
*boundaries* and those who want that pervasively. And for OPT, there are
those who want most of their code sped up and those who wnat only "inner
loops" sped up. You can already see a conflict. People who believe
strongly in DOC are going to want the maximum number of type
declarations and those who are interested in OPT just want to "prime" a
type inferencer with the minimal amount of necessary information.

> 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.

I agree. But I don't think that those of us outside of academia have the
extra bandwidth to take on this project.

> 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.

Agreed. We have historically called this "systems Python" "swallow" but
nobody has ever defined or implemented it. It sounds like a great
project for a graduate student and a great contribution to the Python
community.

I can't get Dejanews to give me the first messages on swallow, but here
are some later ones:

http://www.deja.com/dnquery.xp?ST=MS&QRY=Python+swallow+type&svcclass=dnold&DBS=1

-- 
 Paul Prescod - Not encumbered by corporate consensus
"Computer Associates is expected to come in with better than expected 
earnings." Bob O'Brien, quoted in
	- http://www.fool.com/news/2000/foth000316.htm