Re: Type Analysis

[Mike Pall <mikelu-0508@...>]

Hi,

Rici Lake wrote:
>   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
>
> 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.

Automatically deriving the contract is the most desirable option.
But this is tough for the above function. Apart from requiring
interprocedural analysis it requires quite a bit of knowledge
about the identity and the behaviour of 'type'.

[
This implies that 'type' would be easier to analyze if it was
an intrinsic. But IMHO this isn't too useful in practice. Looking
at quite a few examples, I can't find a single case where the
hints would get more accurate with additional knowledge about
'type' (I already use the result hints for 'type', i.e. that it
returns a string).
]

> If `The' is a library function,
> then the burden of writing contracts falls on the library
> designer rather than the end user.

I did this for most of the standard C library functions.
Only result type hints for forward analysis, though. E.g.:

hintlib("type",        "")
hintlib("string.len",  1)
hintlib("string.sub",  "")
hintlib("math.floor",  1)
hintlib("math.sin",    0.5)
hintlib("math.frexp",  0.5, 1)

It's all in an extra module loaded at -O2.

Proved to be most useful for inlining table lookups with
some hints for the type of the key:

 t[string.sub(s, n, m)] = true
 t[math.mod(x, m)] = x

Not so useful for plain arithmetics since there's no point
in inlining anything else than the numeric case.

> Furthermore, the language
> is free to ignore the contract, but a JIT compiler which
> does type analysis could use it.

I have thought of something like this for inline hints:

if nil then __jit = "off" end

But I haven't implemented it (yet). Needs a bit more thought
to be general enough for parameter type hints and the like.

> 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.

Right now I'm doing (2) for most stuff. A few simple idioms
use (1). I'm not doing MFP (yet).

Still, the generated hints are quite accurate and the runtime
contract verification has little overhead. I tried removing all
type checks and got only a few percent speedup in non-contrived
cases (yes, mandelbrot is contrived ;-)).

I'm not too fond of (3), but some manual contracts are inherently
of this type. E.g. the ackermann benchmark would benefit most
from an 'integer' type hint. I cannot think of a way the compiler
could infer that this function works fine with integers (instead
of doubles) for a given set of parameters. But it would be a lot
faster with integers, of course (and the spec allows it).

Most interesting would be to backpropagate contracts as far as
possible (i.e. out of the inner loops). In the best case the
contract could be verified at the start of the function (or its
caller and so on).

Instead of branching to (mostly unused and expensive to generate)
fallback code it could just force recompilation with an additional
'contract broken' hint. This would either lead to generalization
or to more specialization.

But I'm not at that point yet.

> 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 ... )

Comments don't go through to the bytecode ...

Bye,
     Mike