Type Analysis

[Rici Lake <lua@...>]

On 28-Aug-05, at 8:17 AM, Mike Pall wrote:

> Often enough a comparison is the key hint you need for the
> analysis of a freestanding function. In the context of a JIT
> compiler you get most type hints from passed parameters of
> course (but these are only hints and must be checked at runtime).
>
> While I'm at it, I should note that the addition of generic
> metatables weakens the precision of the analysis in some cases.
> E.g. one can no longer infer that obj in 'obj:method()' must be
> a table or userdata (which allowed some shortcuts).

Maybe so, but I've become quite enamoured with the : syntax for
string operations, particularly as it allows the possibility of
creating polymorphic code working with "string-like" objects
(input streams or string buffers, for example).

In passing, I note that:

  function interleave(a, b)
    if type(a) == "number" and type(b) == "number" then
      -- do something
    else
      error("Expected two numbers, got (`"
             ..type(a).."', `"..type(b).."')")
    end
  end

is "better" (and the equivalent would be normal in a
C binding), and provides a more-or-less absolute guarantee
about a and b in the then clause (subject to redefinition
of the global "type").

However, it's really bulky to write; in practice, I might use

  function interleave(a, b)
  local na, nb = assert(tonumber(a)), assert(tonumber(b))⊥⊥

but you can get slightly better error messages from

  function interleave(a, b)
  local na, nb = The("number", a), The("number", b)

And that has gotten to a point where program analysis would
be simple, given the contract that The("type", foo) either
produces a value of the given type or throws an error. [Note 1]

  function The(t, a, err)
    if type(a) == t then
      return a
    else
      err = err or "Bad value"
      error(err.." ("..t.." expected, got "..type(a)..")", 2)
    end
  end
  -- [Note 2]

I think the notion of "contract" is interesting here. (Indeed,
it's an interesting concept in general.) In this context, I
only need to provide a contract for `The' and type analysis
would be able to do the rest. If `The' is a library function,
then the burden of writing contracts falls on the library
designer rather than the end user. Furthermore, the language
is free to ignore the contract, but a JIT compiler which
does type analysis could use it.

In such a case, it would have a few options: (1) prove the
contract; (2) verify the contract; (3) produce incorrect code
if the contract were violated. Option (3) would be irritating,
but acceptable if the JIT were optional, I suppose.

I'm not going to provide any syntactic suggestions, but they
abound in other languages. Pseudo-comment syntax, however, would
make the optionality clear. (eg. --#contract ... )

R.

[1] I borrowed the word "The" but not the semantics from a
standard primitive in functional programming languages. The
standard semantics would be to return bottom (⊥) (or equivalent)
rather than throwing an error.

[2] A number of improvements suggest themselves, such as allowing for 
numeric conversions, improving the quality of the error messages, etc.