[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: cheerful static typing (was: Any and Every... (was: Eval))
firstname.lastname@example.org (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.)