[Types-sig] RFC 0.1

[John Ehresman]

On Mon, 13 Dec 1999, Guido van Rossum wrote:
> ...
> OK.  I'm not sure everywhere whether you want compile-time or run-time
> checking.

I think it might be possible to do both run-time and compile-time
checking by defining the system in terms of what happens at run time, but
allowing compile time optimizations to be made.  For example, we might
say the declaration (using C-like syntax) "def IntType atoi(StringType
s):" to mean that if a value is passed to atoi that is not a string, a
TypeError exception is raised.  This declaration might be enough for a
lint like program to analyze code before it is run and to flag cases where
TypeError would be thrown.  I think there's value in having run-time
checking to support delayed checking in some cases -- it would allow
strongly typed functions to be bound to symbols without any typing info.
Otherwise, it unclear how to handle the following:
  def IntType atoi(StringType s):
    ...

  if something:
    conv = atoi
  else:
    conv = function_of_unknown_type
  print conv('1')

Then, if a compiler was able to determine that the value bound to
StringType never changed and that a value was a valid StringType, it could
optimize away the code to check the type of that value.  This could be
implemented for functions by separating the code to check argument types
from the function body and setting up the calling conventions so that the
type checking code was only executed when needed.

I don't see anything here that prevents type inferencing to work in either
a lint like program or a compiler.  For example, from the code:
  def IntType atoi(StringType s):
    ...

  def wrapper(s):
    return atoi(s)

it's relatively easy to determine that wrapper must take a string and
returns an integer (assuming the binding for atoi is constant).

John