Re: From dynamic to static

[Rici Lake <lua@...>]

On 31-Oct-05, at 4:51 PM, David Given wrote:

> You'd also need a limitation on variable assignments to one particular 
> type.
> So:
>
> local foo = 7
> foo = "bar"
> ...would fail a type constraint.

I don't see why, except for trying to do "static" type checking. You 
could equally well check the assertion that foo has the correct type at 
every use-point, which would mean keeping track of the (set of) types 
foo might contain at the entry to each basic block. If you know the 
(possibly generic) function prototypes of every function, you could 
pull that off, and if you didn't know that, you wouldn't be able to 
accomplish this:

> However, this also means that:
>
> local foo = 7
> foo = bar()
>
> ...would mean that, for it to be valid, bar() must return a number.

This sort of thing is done by some Scheme compilers, for example. Lua 
goes out of its way to make it difficult, of course, because it is very 
hard to track assignments to closed variables. But you don't have to 
get it perfect: you can still insert run-time checks if the compiler 
can't prove that static checks are sufficient. (Dylan does this, and 
the original Apple IDE also colour-coded the program to show you where 
the run-time checks were inserted, in case you felt like adding 
declarations, etc.)

An interesting example of this sort of thing:

...
--[[ line 1 ]]  local a = i
--[[ line 2 ]]  assert(type(a) == "number")
--[[ line 3 ]]  local b = math.sin(a)
--[[ line 4 ]]  return b
...

Say that at line 1, the compiler knew that i was a number (perhaps 
because there
was a "local i = 3" somewhere leading up to that point.) In that case, 
it can deduce that a is a number, and the assert check at line 2 is a 
compile-time constant, so it doesn't need to actually be generated. 
Furthermore, it can use a non-checking (i.e. fast) version of math.sin 
(if it knows that the math table hasn't been altered), and it can 
demonstrate to itself that the function returns a number, assuming that 
there are no other return statements.

OK, suppose it couldn't prove anything about i. In that case, it would 
have to compile the test at line 2, but it would still know that a was 
a number at line 3, and it would still be able to demonstrate that the 
function returns a number.

Now, suppose the programmer hadn't put in the assert statement. In that 
case, the compiler would pretty well have to do it itself, or it would 
have to use a version of math.sin which did that. However, it could 
still conclude that the function returns a number. In that case, 
hypothesizing a sufficiently integrated IDE, it could even suggest to 
the programmer that the assert() be made explicit, which might be a 
clue to investigate why it wasn't possible to demonstrate that i was a 
number.

Although this seems like more work for the compiler, I think it makes 
for a more interesting programming environment than "static 
type-checking".


> You know, this actually sounds *possible*. Good grief.

Sure. But it also sounds like a different language :)