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

Daniel Wang danwang@CS.Princeton.EDU
11 Jul 2000 15:04:28 -0400

Hmmm given the responses, I don't think I made myself all that clear...

Baiscally it boils down to the fact that adding any sort of typing
discipline for what ever reason to "full Python" is going to be a very hard
thing to do. So, I'm basically asking what's a small and interesting chunk
of the language to tackle first. From this small chunck one can very easily
automatically define the appropiate runtime coercions so that when you cross
over into the rest of Python there is an extra runtime check inserted at the
right places. 

Then the big picture is to slowly grow this chunck of typeable Python into
more and more of the full language. Ideally the subset of typeable Python is
really a subset of full Python, with perhaps an extra interface description
file to prime the type inference system and to provide module level
interface documentation.

For example, I can easily see doing the procedural subset of Python without 
classes in a relatively easy way. 

Also if you have a well defined static core it's easy to have this core
interoperate with the existing very dynamic features of Python.

The issue number 5. "Large enough not to hide any of the typing
difficulties." Is really an issue about how to type the native dictionary
Python types. Doing so will require some relatively novel typing techniques,
but I think they can be handled. I'd like to let people use normal Python
idioms and still have dictionaries "just work". 

It be nice to have a dictionary type that could state an invariant of the

  If you pass this dictionary a symbol with the value "x" it will return a
  value of the type int or string, pass it the value "y" and you will get
  the value 1.

Which, would look something like

  { S("x") -> (int | string),
    S("y") -> S(1)}

You should read S(v) as the singleton type which is a type that contains
exactly one element whose value is "v". The question to ask is whether this
sort of very fine grain type information will let you assign types to a very
large subset of Python, and how much of this information can be inferred

Oh well... these are just semi-random thoughts... but I think it be useful
to pick out a subset...