[Date Prev][Date Next][Thread Prev][Thread Next]
- Subject: Re: From dynamic to static
- From: "Mark Meijer" <meijer78@...>
- Date: Tue, 01 Nov 2005 19:45:24 +0000
All that might work to a certain extent as long as everything can be traced
through pure lua code. An interesting thought. But i imagine it gets nigh
impossible as soon as a C function is called anywhere (including standard
library calls). C functions can potentially change anything anywhere in the
entire lua environment, with effects that are completely unpredictable to
the type checker (including types/values that aren't even related to the
current context of the call like arguments, returned values, etc).
Strictly speaking, this means that any C function call in a control flow as
traced by the type checker, would invalidate everything in the type
checker's state that it had gathered up to that point. Also I suspect
metatables can introduce some complexity in this issue, if not
unpredictability. There are ways to formalize this of course and to provide
hints to the checker, but this would probably involve fundamental extensions
to the language, and I don't suspect it's possible to actually enforce it
(which essentially means it would still be unpredictable, at best extremely
From: Rici Lake <email@example.com>
Reply-To: Lua list <firstname.lastname@example.org>
To: Lua list <email@example.com>
Subject: Re: From dynamic to static
Date: Mon, 31 Oct 2005 17:15:03 -0500
On 31-Oct-05, at 4:51 PM, David Given wrote:
You'd also need a limitation on variable assignments to one particular
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
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 :)