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

[neelk@cswcasa.com]

Daniel Wang [mailto:danwang@CS.Princeton.EDU] 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. 

Didn't some Smalltalk people invent Strongtalk? And Common Lisp has
had optional type declarations for ages, a feature which Dylan 
emphasized a lot more in its design. 

Nobody seems to have seized upon Hindley-Milner type inference, but I 
think that without something like Haskell's overloading or ML's functors, 
it's not possible to write sufficently reusable typed software -- and 
both of these are AFAIK very recent innovations. But I digress, and am
probably retreading ground very familiar to you....

> 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

What you want to look at is Oaklisp. It's basically Scheme with
Python's OO system fully integrated into the language. (It actually 
predates Python, but my meaning should be clear.)

I this that this will let you reuse much of Scheme's denotational
semantics when defining your static Python subset. If you want, I'd
be delighted to help, though everything I know about language theory
is self-taught and likely weirdly incomplete.

This also implies making some changes to core Python's semantics, such
as adding lexical scoping and eliminating the type/class distinction,
but both of these are widely (but not universally) regarded as 
good additions.

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

Throw in ML's functors and I'm sold. They are so clearly the Right 
Thing it's not funny. :)

--
Neel Krishnaswami
neelk@cswcasa.com