[Types-sig] recursive types, type safety, and flow analysis (was: Recursive types)

[Greg Stein]

On Tue, 21 Dec 1999, Guido van Rossum wrote:
> > From: Greg Stein <gstein@lyra.org>
> > 
> > On Tue, 21 Dec 1999, skaller wrote:
> > >...
> > > 	If I may: there is an issue here which
> > > some people may not have realised: recursive types.
> > 
> > These are not possible in Python because definitions are actually
> > constructed at runtime. The particular name/object must be available at
> > that point in the execution.
> 
> Huh?  "Recursive types" typically refers to all sorts of nodes, graphs
> and trees (where an instance attribute has the same type as its
> container).  Certainly these are possible in Python!

True... I use the stuff, too...

I should have clarified that I don't think his particular example would
work because of the compile- / definition- time recursion of the names.
Runtime? Sure. It's fine.

> > > In an interface file, this can be handled by 
> > > two passes.
> > > 
> > > 	In implementation files, it is much
> > > harder, since scoping rules are dynamic.
> > > This is a good argument for interface files.
> > > Example:
> > > 
> > > 	class X:
> > > 		def f(y:Y): ...
> > 
> > This fails. Y is not defined.
> 
> If I understand the context correctly (X defined before Y but using Y)
> I disagree.  Since this works fine without type declarations (as long
> as the instantiations happen after the classes are defined) I don't
> see why adding static typing should break this.

Because Y is not defined. This is analogous to the following code:

class Foo:
  def build_it(self, x, y, cls=Bar):
    return cls(x, y)

class Bar:
  ...

The above code breaks. I am positing that if you put "Y" into a
declarator, then it should exist at that point in time. Where "time" is
specified as following the flow of execution as the functions/classes are
defined.

> Also, I think that static typing should have a much more liberal view
> about forward referencing than Python itself.  Since it is quite legal
> to have
> 
>   def f(): g()
>   def g(): ...
>   print f()
> 
> I think that typecheckers should deal with this, and not complain
> about the forward reference to g in f!  (Except when f is called
> before g is defined.  Flow analysis should allow this distinction.)

Good point.

I don't think we can detect that call-before-definition, though.

I think your point can be restated as: Can we type-check the following
code?

def f() -> String:
  return g()

def g() -> String:
  ...


I haven't thought about this particular scenario or the resulting impact
on the inferencer. We probably require some kind of a two-pass analysis as
John points out. Maybe it is as simple as deferring analysis of function
bodies until the global "body" is analyzed. Actually, I think the deferral
mechanism is sufficient, as that mirrors the execution environment: at the
time the function body is executed, the globals are defined.
[ with the caveat of call-before-define, but we can't determine that ]

Hrm. The whole call-before-define problem might actually axe Paul's desire
for type safety. I don't think we can *ever* guarantee that a name will
exist at the time it is used. For example:

value = 1
def typesafe f():
  somefunc(value)

del value
f()

If you start doing *control* flow analysis, then you might be able to
definitely state the above code is in error. But then, I'll just throw
this wrench at it:

if sometest():
  del value
f()

Now what?

The type inferencing that I believe we can/should be using is based on
some basic data flow, without regard to definitively determining whether a
particular branch is reached or not. If a possibility exists, then the
possible types are unioned in. If type-safety is defined as "no
NameErrors", then we have a problem, as control flow is required.

Note that I believe the following can be handled:

value = 1
def typesafe f()
  func_taking_int(value)

value = "foo"
f()

In this case, the global variable "value" has a typedecl of: Int or
String. This would fail the func_taking_int() function call.

Back to the other point: I do believe that you should not use a name in a
type-declarator if it isn't defined.

Cheers,
-g

-- 
Greg Stein, http://www.lyra.org/