[Types-sig] Proposed Goals PEP

[Tim Hochberg]

> Constraints:
>
> In order to get something done in a reasonable amount of time we must
> decide which issues not to tackle. At the top of that list, in my
> opinion, is static type checking (including a formally defined type
> inferencing system). Second is any form of higher order types. If we
> could agree that these are NOT on the table we will make progress much
> more quickly.
>
> In general, a major constraint is that a type system for Python should
> be simple. We should not be afraid to teach the type system to high
> school students. If Python's type system makes anyone's brain explode
> then we have not done a good job.

First off: thanks for getting this going again Paul; I know it's a thankless
job.

Before things get too set in stone (or too chaotic), let me throw at a
slightly different approach. That is to provide the machinery for type
checking with essentially no formal type system at all.

THE BASICS

Consider this code (syntax borrowed from one of Guido's old proposals):

def spam(eggs : Integer, beans : File) -> String:
   #....
   return x

This would be compiled to:

def spam(eggs, bakedBeans):
   if __typecheck__ and not Integer.check(eggs): raise
TypeError("Informative message here")
   if __typecheck__ and not File.check(beans): raise TypeError("Informative
message here")
   # ...
   if __typecheck__ and not String.check(x): raise TypeError("Informative
message here")
   return x

Note that Integer, File and String are all bound when the def is executed,
just like default argument are now. Also, __typecheck__ is magic variable
similar to debug so that typechecks can be omitted completely during
compilation so that there is no speed penalty when compiled this way.

The above has the great strength that it's easy to explain! I also believe
that it can support a rich, runtime type system (err) and is useful for doc
as well. It's utility may well be limited for opt and glue though.

In addition to the above syntax, _some_ type support would be included. This
would consist of typecheck objects for the basic types (int, string,
complex, etc). One possibility would be to add this information to the
TypeObjects in the types file, but for the moment I'm going to assume that
they would a separate object. Consider Integer as rendered in Python:

class Integer:
   "A builtin, machine size integer"
   name = "Integer"
   def check(self, object):
      return isinstance(object, types.IntType)
Integer = Integer()

Note that it has a docstring and a name field, documentation extraction
tools could extract this information for documention purposes. That's not so
strong an argument for integers, but useful for more complicated types. For
the time being I'll assume that this information lives in the typecheck
module.

Already this is provides simple type checking fot the basic types, but we're
just getting started....

PARAMETERIZED TYPES

Parameterized types are easy to support in this model, although the checks
are potentially very expensive. Consider a parameterized list type:

class ListOf:
   "A parameterized list of objects"
   def __init__(self, type):
      self.type = type
      self.name = "ListOf(%)" % type.name
   def check(self, object):
      if not isinstance(object, types.ListType): return 0
      for item in object:
         if not self.type.check(item): return 0
      return 1

Which could be used as:

from typecheck import Integer, ListOf

def integralSum(l : ListOf(Integer)) -> Integer:
   "Return the sum of the integers in l"
   # ....

COMPOSITE and CUSTOM TYPES

One can easily define composite types in this framework as well. I'm not
sure how far we should directly support this sort of stuff at first, but
it's comforting to know that the possibility is there. Here's an example of
a generic custom type:

class CompositeOf:
   "A composite type"
   def __init__(self, *types):
      self.types = types
      self.name = "CompositeOf(%s)" % ", ".join([t.name for t in types])
   def check(self, object):
      for t in types:
         if types.check(t): return 1
      return 0

Used like:

from typecheck import Integer, String, CompositeOf

def iTakeAnIntOrAString(x : CompositeOf(Integer, String)):
   #...

Custom types such as odd integers would also be easy to define. The way that
these more complicated types fall out of a simple proposal makes this feel
very pythonic to me.

INTERFACES

I'm guilty of not looking at the interface proposals in any detail, but
presumably this proposal and/or interfaces could be munged so that
interfaces would be acceptable type parameters. One approach would be just
to give interfaces a check method.

SUMMARY

This idea looks like a good starting point to me. It's simple, it can
express complex types, it helps both err and doc. On the downside, it's
unlikely to help opt, and I don't know about glue.


Regards,
-tim