[Types-sig] recursive types, type safety, and flow analysis

[Greg Stein]

On Wed, 22 Dec 1999, Paul Prescod wrote:
>...
> The problem is that you and I are thinking about a Algol-style type
> checker. Greg is talking about a complex, sophisticated type inferencer
> that tries to understand what your Python code *means*. I am only

"Means"? Not at all. I'm only suggesting we watch what happens with the
types. We have to do that *anyhow* to do the type checking.

You're saying we declare types up front and verify them when we run into
the name. To verify it, that implies we need to know the implicit typedecl
when we find the name.

I'm saying we use the implied typedecl.

Why make it explicit, when we have all the information we already need?

>...
> > I like the idea better (I think proposed by Tim Peters) that the names
> > used for type declarations live in a separate compile time namespace
> > where different rules apply.  (Even though there are obvious
> > correspondences, e.g. the names of defined or imported classes should
> > probably be available both at compile time and at run time.)
> 
> I agree. We will soon have to move forward on this basis.

As long as we have a solution for making the typedecl objects available at
runtime. If we are introducing type information to Python, then we ought
be able to introspect on that information.

> The static type checker is a very different tool and it does not, in
> general, try to understand "Python code."

It has to understand it to some level to ensure that your types are used
properly. There is no avoiding that.

I think you're assuming there is too much of an increment between type
checking and the level of inference that I'm proposing (actually,
"deduction" as John would call it).

> Two *convenient exceptions*
> are top-level class and function declarations. But these are just
> convenient exceptions. I feel strongly that this:
> 
> if doSomething():
> 	class a:
> 		def doSomething(self):
> 			pass
> else:
> 	class a:
> 		def doSomething(self):
> 			pass
> 
> is NOT TYPE CHECKABLE because we do NOT do data-flow analysis.

I think we do. Not pure data flow in the classic sense, but really type
flow. We are doing that anyhow as part of the checking. With declared
names, the scope of your type analysis can be minimized (i.e. on a
per-statement level rather than per-function).

Cheers,
-g

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