[Types-sig] Static typing: Towards closure?

[Guido van Rossum]

> From: scott <scott@chronis.pobox.com>

> 			       -------
> Also, I have some general comments and questions about your proposal:
> 
> 			      *optional*
> In reading your proposal, you make multiple references to an
> "unmodified interpreter" and to having mutltiple grammars.  I
> understand that this is an intuitive response to making static type
> checking optional in python, but I think it is not feesible given
> your 'typecase' strawman slide.  
> 
> I have been struggling with this 'typecase' issue with many different
> approaches and have come to the conclusion that if a type checker is
> going to allow OR'd types, and that type checker is going to
> distinguish confusion between those OR'd types on the part of a
> programmer, then something like a typecase operator is fundamentally
> necessary.  Furthermore, if a program utilizes something like a
> typecase operator, then the program must have access to the
> declarations at run time, even if the type checking is optional.  For
> me, this redefines 'optional' to mean 'you can use these constructs if
> you want', not 'you can use this interpreter and your type errors will
> be reported, otherwise you can use an unmodified interpreter on the
> same program'. 
> 
> This new definition of 'optional' seems fitting to the word and
> acceptable to me, but more subtle than offering the option of using a
> different interpreter.  Do you agree?

I couldn't agree more.  The whole idea of "optional static typing"
always meant that when you were ready for it, you could simply
sprinkle some decl statements in your source code and the interpreter
would start static typechecking for you.  It would be a standard part
of the standard language implementation.  (Probably in Python 2.0, aka
Python 3000.  (Version numbers with 2000 in then are soo last
millennium... :-))

Of course, while we're experimenting with all this, the new syntax may
require early adopters to use a special implementation.  Maybe we're
naive in believing that it would be as simple as deleting all lines
that begin with decl...  But for a reasonable subset of the proposal
(obviously not including typecase or the ! operator) that's possible.

> 			   *paramterization*
> your section on parameterization uses the example of classes, when
> use of a type paramater is potentially widely available to functions
> and built in container types like lists and tuples.  I believe a more
> general form of 'paramterization' which works along the lines of ML's 
> "'a", "'b", etc is quite feasible for a static type checking system,
> as it would involve just a few additional checks and operations in the
> most atomic type checking functions.  Please take into account in the
> design for paramterization that it should be available for more basic
> types than classes.  ML has remarkably clean treatment of the idea,
> btw.

I'm not familiar with ML's 'a, 'b and I don't quite understand what
you are saying here.  In the long form of the proposal there's some
text about parameterized functions, e.g.:

def foo<T>(a: T, b: T) -> T: ...

The builtin types are all supposed to be derived (somehow!) from
parameterized interfaces, e.g.

interface sequence<T>:
    __getitem__(int) -> T
    __setitem__(int, T)
    append(T)
    expand(sequence<T>)
    # or perhaps:
    expand(SELFTYPE)
    # etc.

> 			 *Constructors*
> your type proposal seems to mysteriously be missing the notion of 
> type constructors, that is, something like this:
> 
> datatype FOO = Int | None
> datatype BAR = Int | None
> 
> decl a: FOO
> decl b: BAR
> 
> a = 1
> b = a # ERROR!

Actually, in my mind, this would be allowed.  I believe in structural
type matching, not matching by name.  (That's what I've been
believing, anyway.)  Possibly when you introduce classes there's no
way to have another class match even if it has the same structure,
but for simple unions I don't see the need.  (Or is your "datatype" a
special declaration different from my typedef, which I spell

decl FOO = int | None

?)

> b = BAR(a) # ok, explicit cast or 'constructor'
> 
> It is possible to parse the cast at compile time, since it requires
> no knowledge of the value of `a', only it's type.
> 
> The above example is slightly contrary to a grammar I put together, 
> and I don't believe it's the right way to denote constructors, but it
> does demonstrate the intended semantics.
> 
> using constructors can make dealing with logically OR'd types much
> easier and cleaner, and allows the user to define more specific types
> than allowed with builtin types.  I think it's quite a worthwhile pursuit.

I have chosen names for the std types that are the same as existing
built-in functions, because I want to get a similar effect.  E.g.

x = int(y)

is currently a call of the built-in function int() which happens to
return its argument converted to an int, or die with an exception; in
the new system, it would have the same effect but it would be a
constructor for the int datatype (and the built-in object int would be
the same object as types.IntType).

It's true that these constructors have something of a dynamic cast in
them (they can fail if the argument is unacceptable).  I think that in
my proposal,

x = int(a)

would have about the same semantics as Greg's

x = a ! int

--Guido van Rossum (home page: http://www.python.org/~guido/)