[Types-sig] Revive the types sig?

[Paul Prescod]

I have been involved with the types-sig for a long time and it has
consumed countless hours out of the lives of many brilliant people. I
strongly believe that it will only ever work if we change some of
fundamental assumptions, goals and procedures. At next year's
conference, I do not want to be at the same place in the discussion that
we were this year, and last year, and the year before. The last time I
thought I could make progress through sheer effort. All that did was
burn me out and stress out my wife. We've got to work smarter, not
harder.

The first thing we need to adjust is our terminology and goals. I think
that we should design a *parameter type annotation* system that will
lead directly to better error checking *at runtime*, better
documentation, better development environments an so forth. Checking
types *at compile time* should be considered a tools issue that can be
solved by separate tools. I'm not going to say that Python will NEVER
have a static type checking system but I would say that that shouldn't
be a primary goal.

I've reversed my opinion on this issue. Hey, even Guido makes mistakes.

I think that if the types-sig is going to come up with something
useful this time, we must observe a few principles that have proven
useful in developing Python:

1. Incremental development is okay. You do not need the end-goal in
mind before you begin work. Python today is very different than it was
when it was first developed (not as radically different than some
languages, but still different).

2. It is not necessary to get everything right. Python has some warts.
Some are easier to remove than others but they can all be removed
eventually. We have to get a type system done, test it out, and then
maybe we have to remove the warts. We may not design a perfect gem from
the start. Perfection is a goal, not a requirement.

3. Whatever feature you believe is absolutely necessary to a decent
type system probably is not. There are no right or wrong answers,
only features that work better or worse than other features.

It is important to understand that a dynamically-checked type
annotation system is just a replacement for assertions. Anything that
cannot be expressed in the type system CAN be expressed through
assertions.

For instance one person might claim that the type system needs to
differentiate between 32 bit integers and 64 bit integers. But if we
do not allow that differentiation directly in the type system, they
could do that in assertions. C'est la vie.

This is not unique to Python.  Languages like C++ and Java also have
type test and type assertion operators to "work around" the
limitations of their type systems. If people who have spent their
entire lives inventing static type checking systems cannot come up
with systems that are 100% "complete" then we in the Python world
should not even try. There is nothing wrong with using assertions for
advanced type checks. 

For instance, if you try to come up with a type system that can define
the type of "map" you will probably come up with something so
complicated that it will never be agreed upon or implemented.
(Python's map is much harder to type-declare than that of functional
languages because the function passed in must handle exactly as many
arguments as the unbounded number of sequences that are passed as
arguments to map.)

Even if we took an extreme position and ONLY allowed type annotations
for basic types like strings, numbers and sequences, Python would 
still be a better language. There are thousands of instances of these 
types in the standard library. If we can improve the error checking 
and documentation of these methods we have improved on the status 
quo. Adding type annotations for the other parameters could wait 
for another day.

----

In particular there are three features that have always exploded into
unending debates in the past. I claim that they should temporarily be
set aside while we work out the basics.

 A) Parameterized types (or templates): 

Parameterized types always cause the discussion to spin out of control
as we discuss levels and types of
parameterizability. A type system can be very useful with
parameterization. For instance, Python itself is written in C. C has no
parameterizability. Yet C is obviously still very useful (and simple!).
Java also does not yet have parameterized types and yet it is the most
rapidly growing statically typed programming language!

It is also important to note that parameterized types are much, much
more important in a language that "claims" to catch most or all type
errors at compile time. Python will probably never make that claim.
If you want to do a more sophisticated type check than Python allows,
you should do that in an assertion:

assert Btree.containsType(String)

Once the basic type system is in place, we can discuss the importance
of parameterized types separately later. Once we have attempted to use
Python without them, we will understand our needs better. The type
system should not prohibit the addition of parameterized types in the
future. 

A person could make a strong argument for allowing parameterization
only of basic types ("list of string", "tuple of integers") but I
think that we could even postpone this for the future.

 B) Static type checking: 

Static type warnings are important and we want to enable the development
of tools that will detect type errors before applications are shipped.
Nevertheless, we should not attempt to define a static type checking
system for Python at this point. That may happen in the future or never.

Unlike Java or C++, we should not require the Python interpreter
itself to ever reject code that "might be" type incorrect. Other tools
such as linters and IDEs should handle these forms of whole-program
type-checks.  Rather than defining the behavior of these tools in
advance, we should leave that as a quality of implementation issue for
now.

We might decide to add a formally-defined static type checking to
Python in the future. Dynamically checked annotations give us a
starting point. Once again, I think that the type system should be
defined so that annotations could be used as part of a static type
checking system in the future, should we decide that we want one.

 C) Attribute-value and variable declarations: 

In traditional static type checking systems, it is very important to
declare the type for attributes in a class and variables in a function. 

This feature is useful but it is fairly separable. I believe it should
wait because it brings up a bunch of issues such as read-only
attributes, cross-boundary assignment checks and so forth.

I propose that the first go-round of the types-sig should ONLY address
the issue of function signatures.

Let's discuss my proposal in the types-sig. Executive summary:

 * incremental development policy
 * syntax for parameter type declarations
 * syntax for return type declarations
 * optional runtime type checking
 * goals are better runtime error reporting and method documentation

Deferred for future versions (or never):

 * compile-time type checking
 * parameterized types
 * declarations for variables and attributes

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

-- 
Python:
    Programming the way
    Guido
    indented it.