[Types-sig] how to do a typecase?

[Greg Stein]

What are you guys mumbling and bumbling about? My *prototype* already
handles the code below. It knows "y" becomes and int, and it knows that
"x" is being assigned an integer.

In other words, the whole notion of "we should only be burning time on
[declaring everything first]" is a moot point. We already have an example
that performs "inter-statement inference", and we already have "code out
there". We don't have to declare everything.

Tim: you're trying to simplify where it isn't needed
John: you're trying to make a non-existent problem harder

Cheers,
-g


On Tue, 25 Jan 2000, Tim Peters wrote:

> [Tim]
> >> Bingo.  Checking that use matches declaration is easier than
> >> inferring declaration from use.  "Mere checking" is hard enough
> >> for a first version, though!
> 
> [John Skaller]
> > I don't think these two things are separable.
> > Consider:
> >
> > 	decl x : int
> > 	y = 1
> > 	x = y
> >
> > How can you check y = x, if you do not infer the type of y?
> 
> You're still in the inference game here.  Add
> 
>     decl y: int
> 
> too and checking "x = y" is a trivial local operation.  It does take *some*
> smarts to verify that "y = 1" is cool.
> 
> > The RHS of an assignment is an EXPRESSION: the type of the
> > expression MUST be deduced in order to check that it is
> > compatible with the LHS variable.
> 
> Sure.  The difference is that in the presence of explicit declarations,
> control flow is taken out of the picture (there is no (relevant) control
> flow *within* a Python expression).  Only part of the undecidability of rich
> type systems is due to the undecidability of hairy unifications of type
> expressions; another part is due to the static undecibability of control
> flow; I suspect (but don't know) that part of the reason Haskell's inference
> is bulletproof despite the richness of its type system is that, as a
> functional language, it has no control flow to worry about (there are no
> *dataflow* equations to solve, only type unifications; inference in Python
> suffers full-blown exposure to both).
> 
> There is certainly no hope for building an inference engine if there's no
> hope for solving the static "mere checking" sub-problem.  Solving *only* the
> latter is *sufficient* for ERR and OPT (and is the whole point of DOC),
> although it's not as *convenient* as you (Guido either, for that matter)
> would like.
> 
> Nevertheless, it still needs to be solved, as it's the foundation on which
> everything else stands (or falls).  Every time inter-statement inference
> gets dragged into this, it just strikes me as distraction from getting the
> initial design specified and the initial work done.
> 
> > In the very simplest of cases, where the types of all identifiers
> > (including all functions) are known
> 
> Which is indeed the only thing I think we should be burning time on now.
> 
> > and monomorphic,
> 
> Scott makes a decent case for restricting attention to that too at first.
> 
> > a single bottom up pass will compute the type of any expression.
> 
> So let's do that, get the code the out there, and generalize later.
> 
> > ...
> > As soon as ANY untyped identifier enters the picture, we're
> > stuffed.
> 
> The extent to which that's true also defines the extent to which it's wise
> to forbid the possibility in the first cut.  Most Python programmers likely
> come from C, C++ and Java, where "declare everything" is absolutely
> required.  They won't feel that a half-assed partial inference scheme is "a
> present", they'll just go "huh?" <0.5 wink>.
> 
> trying-to-do-better-is-a-mistake-so-long-as-we-can't-even-do-
>     half-as-well-ly y'rs  - tim
> 
> 
> 
> _______________________________________________
> Types-SIG mailing list
> Types-SIG@python.org
> http://www.python.org/mailman/listinfo/types-sig
> 

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