[Types-sig] how to do a typecase? (was: Static typing: Towards closure?)

[Greg Stein]

On Fri, 21 Jan 2000, Guido van Rossum wrote:
> I finally understand what Greg means when he says "the ! operator
> gives infornation to the typechecker".  In this example:

hehe... see? I still am not clear sometimes.

>...
> the final comment gives us a clue.  Greg wants us to believe that the
> following code should be accepted by the type checker:
> 
>   decl a: int|str
>   decl b: int
> 
>   a!int # "tell the checker a is really an int; exception if we lied"
>   b = a	# not an error according to Greg
> 
> I personally think this is a slippery path that we should not enter at
> all.  What if another thread modifies a before we get to grab it?
> What if we call some function that changes it?  Other questions: what
> if we have an expression designating an item of a dictionary, how
> would we propagate that information?

All these are true, and are mostly related to the fact that "a" is a
global in this case. If you're talking about locals, then the above code
could be fine.

But your point about dictionaries... example:

  x = y[5] ! int
  # what do we know now?

Actually, you're just throwing an issue back at me, when I complained
about:

  if isinstance(y[5], int):

:-)

In other words, 'a!int' *can* say something about a, but the type-checker
will have to apply various restrictions about what it can accept for that
left-hand operand (and still be able to extract meaning). And if those
rules need to be part of the language definition, then I would retract the
issue. (since I'd rather avoid the rules thing...)

> I think that *if* we decide to have x!T in our language, the proper
> definiton for it should be that it raises an exception if the x
> doesn't have type T, and otherwise it yields an expression with type T
> and value x; it should have no other effects on namespaces or
> knowledge of the typechecker.  (The optimizer is a different point,
> but as far as the definition of the language semantics is concerned,
> there is no optimizer.)
> 
> Thus, to make that code pass the type checker, we would have to write
> 
>   b = a!int
>   # a's type is still int|str

I would agree with these two statements.

In certain cases, the code at the top of this email could be accepted, but
to wire that into the definition would imply too many rules and
restrictions (instead of the simple definition for '!' that you just
provided).

And relegating the problem to the optimizer to remove the runtime checks
is perfectly fine with me.

> > "projecting" a type forward from an isinstance() (as you demo above) or
> > within a typecase suite would have similar problems.
> > 
> >   typecase a:
> >     int:
> >       # type-checker labels "a" as an "int"
> >       b = a   # passes
> >       foo()
> >       # what is the type of a?

Note: this was just a demo, regarding the potential changes to "a" by the
foo() function. I do agree that the "int, ai" variant is more robust
against these types of changes.

> > isinstance and '!' seem to be much more clear and robust.
> 
> No, the only robust variant is the typecase syntax I proposed later:
> 
>   typecase a:
>     int, ai:
>       # ai has type int and value a
>       b = ai # passes
>       # b = a # would be an error
>       foo()
>       # ai still has type int

Hrm. True. Even with threading present, the object referenced by "a" can
be pushed on the stack (thus: safe from changes to "a").

The typecase is certainly looking more reasonable to me :-). Especially
based on your quick review of the standard library.

> > And a reminder for ourselves :-) ... we should be careful about labeling a
> > global (at all and/or across a func call).
> 
> I guess by labelling you mean using something like g!T, right?

Sorry... bad wording. I meant we should be careful how the type-checker
records type information for a name.

In my prototype checker, I have been setting it up to automatically create
a union of the types seen for a variable. For example:

  # no decl
  a = 1
  foo()
  a = 'a'
  bar()

For checking purposes, "a" would have int|str. It is somewhat questionable
what the type should be as the global code is being checked; certainly it
would be int|str for the checks of the function bodies.

Cheers,
-g

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