Re: cheerful static typing (was: Any and Every... (was: Eval))

[address@hidden]

gregs@ai.mit.edu (Gregory T. Sullivan) writes:

> Put another way, all programs, for given a static analysis, fall into
> one of three camps:
> 
>   (1) Statically safe - proven to be free of runtime errors.

This isn't necessarily the case.  You can have a `statically safe'
program that `throws an exception' or `invokes the error handler' at
runtime.  You can declare *every* variable in your program of type
`any', and put in the appropriate `type union discriminators'.  Now
the compiler can `prove' that your program is `correct' insofar as the
types go: every expression in your program leads to a defined
behavior.  Of course, one of these behaviors is `invoke the runtime
error handler', but it *is* correctly defined and type safe.

Now in my opinion this simply amounts to saying `that isn't a type
error, it's the default action of the type union discrimination'.

>   (2) Statically unsafe - proven to encounter an error at runtime, 
>       for at least some legal inputs.
>   (3) Not sure.

You can sidestep the issue another way:  restrict the language
such that the only `valid programs' are those in which the static
analysis completes with the answer `true'.  Now you will have some
things that sure *appear* to be programs, even to the sophisticated
user, but they really aren't.

> It is the 3rd class of programs that the programmer (or user) may want
> to have some say in whether they run.

You can sidestep in another way:  make sure there are no undefined
behaviors in the language (for instance, specify that invoking
`length' on a non-composite object throws a `non-composite object
exception', etc. etc.)