[Types-sig] RFC 0.1

[Martijn Faassen]

Greg Stein wrote:
> 
> On Wed, 15 Dec 1999, Martijn Faassen wrote:
> > Paul Prescod wrote:
> > > Martijn Faassen wrote:
> > > > I agree with this, which is I am advocating a strong split (for
> > > > simplicity) of fully-statically checked code and normal python code.
> > >
> > > I don't see this as buying much simplicity. And I do see it as requiring
> > > more work later. I also see it as scaring the bejeesus out of many
> > > static type system fence sitters. Can you demonstrate that it makes our
> > > life easier to figure out integration issues later?
> >
> > Sure, but we're bound to scare the bejeesus out of everyone anyway;
> > we're proposing a major change to Python.
> 
> "We" ?
> 
> I'm advocating a minimal change.

Ahum:

> Add a bit of grammar to function
> definitions. Add a new type-assert operator. Add Tim's "decl" statement
> for interfaces (caveat/todo: rationalize against JimF's proposal). Leave
> out the complexity of variable declarations.
> 
> Note that I'd be okay with punting the "decl" / interfaces for now. That
> leaves a bit of "def" grammar changing and a new operator.
> 
> To the Python programmer: *very* little change.

The programmer needs to deal with the following new things and their
consequences:

* New grammar with function definitions.

* A whole new operator (which you can't overload..or can you?), which
does something quite unusual (most programmers associate types with
names, not with expressions). The operation also doesn't actually return
much that's useful to the program, so the semantics are weird too.

* Interfaces with a new 'decl' statement. [If you punt on this you'll
have to the innocent Python programmer he can't use the static type
system with instances? or will we this be inferenced?]

* Unspecified syntax to actually *specify* types, I mean, a ! operator
with
something syntactically wholly new behind it may not be that simple for
the Python programmer either. It's not that hard with IntType and so on,
but it gets complex if you have function types, class types, etc.

* And then there's the type inferencer which will interact with the
Python programmer's code as well, right? And the interpreter will spew
out errors if compile time checks fail on types?

And you call this: '*very* little change' ? I'll call adding a list with
names of static type associations to the module an 'an even *smaller*
change' then, as you don't need any new operator or statement, at least
to start with. :)

Adding anything like static type checking to Python entails fairly major
changes to the language, I'd think. Not that we shouldn't aim at keeping
those transparant and mostly compatible with Python as it is now, but
what we'll add will still be major.

> > The 'simplicity' part comes in because you don't need *any* type
> > inferencing. Conceptually it's quite simple; all names need a type.
> 
> 1) There is *no* way that I'm going to give every name a type. I may as
>    well switch to Java, C, or C++ (per Guido's advice in another email :-)

Sure, but we're looking at *starting* the process. Perhaps we can do
away with specifying the type of each local variable very quickly by
using type inferencing, but at least we'll have a working
implementation!
 
> 2) You *still* need inferencing. "a = foo() + bar()" implies that some
>    inferencing occurs.
>    (for a compile-time check; the compiler can insert a runtime check to
>     assert the type being assigned to "a" (but you know my opinion
>     there...))

Sure, that's true.

[me]
> > > > Later on you can work on blurring the interface between the two. First
> > > > *fully* type annotated functions (classes, modules, what you want),
> > > > which can only refer to other things that are fully annotated. By 'fully
> > > > annotated' I mean all names have a type.

[Paul]
> > > I think that's a non-starter because it will take forever to become
> > > useful because the standard library is not type-safe. Anyhow I fell like
> > > I've *already solved* the problem of integration so why would I undo
> > > that?
> 
> Agreed. Also, if I grab some module Foo from Joe, and he didn't add
> typedecls, then why shouldn't I be able to use it?
> (and I'd just add some type-asserts if that even mattered to me)

I'm not saying this is a good situation, it's just a way to get off the
ground without having to deal with quite a few complexities such as
inferencing (outside expressions), interaction with modules that don't
have type annotations, and so on. I'm *not* advocating this as the end
point, but I am advocating this as an intermediate point where it's
actually functional.

[me]
> > > > Our static type checker/compiler can use the Python type constructions
> > > > directly. We can put limitations on them to forbid any type
> > > > constructions that the compiler cannot fully evaluate before the
> > > > compilation of the actual code, of course, just like we can put
> > > > limitations on statically typed functions (they shouldn't be able to
> > > > call any non-static functions in the first iteration of our design, I'm
> > > > still maintaining)
> 
> The compiler can issue a warning and insert a type assertion for a runtime
> check. IMO, it should not forbid you from doing anything simply because it
> can't figure out some type. Python syntax's "type agnosticism" is one of
> its major strengths.

Yes, but now you're building a static type checker *and* a Python
compiler inserting run time checks into bytecodes. This is two things.
This is more work, and more interacting systems, before you get *any*
payoff. My sequence would be:

* build system that can do compile-time checking of fully annotated code

   * now you can work on interfacing this with non-fully annotated code.
You
     can also looking at including run-time assertions.

   * in parallel, now you can work on type inferencing the local
variable               annotations out of function type signatures,
interface declarations, 
     and so on.

If you don't separate out your development path like this you end up
having to do it all at once, which is harder and less easy to test.

[Paul]
> > > I see no reason for that limitation. The result of a call to a
> > > non-static function is a Pyobject. You cast it in your client code to
> > > get type safety. Just like the shift from K&R C to ANSI C. Functions
> 
> Bunk! It is *not* a cast. You cannot cast in Python. It is a type
> assertion. An object is an object -- you cannot cast it to something else.
> Forget function call syntax and casting syntax -- they don't work
> grammatically, and that is the wrong semantic (if you're using that format
> to create some semantic equivalent to a cast).

This'd be only implementable with run-time assertions, I think, unless
you do inferencing and know what the type the object is after all. So
that's why I put the limitation there. Don't allow unknown objects
entering a statically typed function before you have the basic static
type system going. After that you can work on type inference or cleaner
interfaces with regular Python.

But perhaps I'm mistaken and local variables don't need type
descriptions, as it's easy to do type inferencing from the types of the
function arguments and what the function returns, as well as the types
of any instance attributes involved. I'd like to see some actual
examples of how this'd work first, though. For instance:

def brilliant() ! IntType:
    a = []
    a.append(1)
    a.append("foo")
    return a[0]

What's the inferred type of 'a' now? A list with heterogenous contents,
that's about all you can say, and how hard is it for a type inferencer
to deduce even that? But for optimization purposes, at least, but it
could also help with error checking, if 'a' was a list of IntType, or
StringType, or something like that? It seems tough for the type
inferencer to be able to figure out that this is so, but perhaps I'm
overestimating the difficulty.

Regards,

Martijn