[Types-sig] RFC 0.1

[Paul Prescod]

Greg Stein wrote:
> 
> True, but I might posit that (due to Python's dynamic nature) you really
> aren't going to come up with a good compile-time system. That leaves
> runtime.

Okay, but my mandate is to come up with a static (compile-time) system.
I already have a variety of runtime tools for doing type checking. 

http://www.python.org/sigs/types-sig/

> In Python, names have no semantics other than an identifier, a scope, and
> that they are a reference. We thought it would be nice to retain the
> notion that names are just names -- it is the objects and what you're
> doing with them that is important.

But we WANT some names to have semantics. sys.version should be an
integer. sys.path should be a list of strings. __builtins__.dir should
be object->list and so forth.

> The above code is quite legal in Python (and no, I don't want to hear
> arguments that it shouldn't be :-). 

I am perfectly happy to have it be legal Python code. I just don't
intend for it to be *statically type checkable* Python code. No, you
cannot use all of the flexibility of Python and expect to get all of the
static type checking of Java. For each function you choose one or the
other.

> With a type system that is associated
> with expressions/values rather than names, then we can do proper type
> inferencing, checking, etc on the above code.

That code could not be legally inferenced in any inferencing system I am
familiar with. (ML and inferenced Ada) If you write a formal
specification for "data flow analysis" that can be implemented by two
independent compilers based on the spec then I will take this approach
seriously. But my impression from my time in the scheme world is that
"data flow analysis" is an unconscious code-word for "let's put this
problem off and hope that someone else figures out some magic that I
haven't figured out yet."

If a static type checking system is hard for Python, a static type
inferencing one is going to be doubly hard!

> > Rebinding is fine, as long as it doesn't invalidate the type
> > declaration:
> >
> > abc = lambda: "def"
> 
> So you say :-)  I say rebind all you want. Base your assertions and
> type-checks on what it has at whatever lexical point in your program.

What if the rebinding happened in some other function, class or module?

> I believe that Python is too rich in data types and composition of types
> to be able to add *syntax* for all type declarations. I think you better
> stop and realize that before you get in too deep :-)

I have a few different answers here:

 1. I don't have to be able to describe every possible type. If you
can't statically check that "foo is a callable from T,T to callable from
T" tough bloody luck, at least for the time being. Java can't do that.
Neither could mid-90's C++. And forget about it for ANSI C. 

Python is not the world's most OO programming language. It is just a
good one. It may not have the world's most static type checker. It will
just have a good one. No type system makes type errors impossible so
that is not my goal. My goal is that if a module uses type checks as
religiously as  Java module would, that module would be roughly as
type-safe. 

 2. Python is no richer in types than any other language with an
extensible type system. This includes ML, Haskell and even Java. There
is no language today without a list type or mapping type. Yes, some
Python complexity comes from the fact that there are dozens of
non-reflective types "built-in" but we can and should fix that.

 3. Compositions of types are complex, but not infinitely complex. We
have about two decades in parameterized type research to rely on. Within
a year and a half, two of the world's most popular languages (C++ and
Java) will have parameterized types.

> In your RFC 0.1, you punted on the complex/composited data types issue too
> keep the solution tractable. I posit that you will *never* solve the
> problem of coming up with sufficient syntactical expression; therefore,
> you will always have to resort to a procedural component in your type
> system *if* you want full coverage.

I am happy to have a runtime component. I just don't see that we need
any new syntax for this runtime component. And I don't think that we
should give up on a formally defined static system.
-- 
 Paul Prescod  - ISOGEN Consulting Engineer speaking for himself
Three things to be wary of: A new kid in his prime
A man who knows the answers, and code that runs first time
http://www.geezjan.org/humor/computers/threes.html