Re: integer exponentiation with negative exponent

["Thomas Jericke" <tjericke@...>]

-----Original Message----- 
> From: "Coda Highland" <chighland@gmail.com> 
> To: "Lua mailing list" <lua-l@lists.lua.org> 
> Date: 17-05-2014 15:06 
> Subject: Re: integer exponentiation with negative exponent 
> 
> 
> Well, sure, it's possible to write functions that can't be reasoned
> about. The halting problem proves this is so. But function calls
> aren't fatal issues in and of themselves -- but the static analyzer
> should be able to determine that it KNOWS it can't reason about
> test().
> 
> Or if it's particularly sophisticated it can admit test()'s return
> type as "number" or as "int|float" instead of "int" or "float". It's
> still possible to reason on this signature, since you can at least
> recognize what operations are legal on it.
> 
> If it's EXCEPTIONALLY sophisticated it can recognize that test() has
> bound an upvalue and consider the upvalue to be part of the function
> signature. It can admit a return value of something like "'int' ? int
> : float". 

Wait, you're looking at the values of the input now, not the types. Once you analyze that
you can also analyze x^y for negative values of y. Even though I wonder how that sophisticated static analyzer knows the value of 'int'.

> We're hitting diminishing returns at this point, especially
> since such reasoning can't be done about C functions (at least, not
> without manual annotation)

That's the most common case if I look at the Lua code we use in our projects.

--
Thomas