[Types-sig] Static typing: Towards closure?

[Jeremy Hylton]

>>>>> "GvR" == Guido van Rossum <guido@CNRI.Reston.VA.US> writes:

  [scott writes:]
  >> *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.

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

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

The alternate suggestions I made on your whiteboard before the
bile/gal bladder digression (note to other readers: don't go there :-)
where based on ML's notation.  The key difference is that you don't
use special angle bracket notation to specify which types are type
variables.  Instead, you would write:

def foo(a: 'a, b: 'a) -> 'a:

The ' before the type name would indicate that it is a type variable. 

In ML, the empty list constructor [] (just like Python!) has the type
'a list.  The programmer doesn't need to explicitly declare the type
of a list because it will be inferred from the type of the objects
that are put in the list.

a = [2,3]  : int list
a.append("foo")  # failts because "foo" isn't type int 

The type checker should infer the most general type, so I assume the
following could also be checked:

a = [2, 3.5, 2j+1]  : number list

Jeremy