[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
cheerful static typing (was: Any and Every... (was: Eval))
I've greatly enjoyed reading this list so far. Thanks!
The discussion about `any' and `every' has got me thinking about something.
Static type-checkers typically act "pessimistically". That is: a typical static
type-checker rejects code which might be correct, but which it can't statically
prove to be correct. For example, suppose there is a function `f' statically
declared to return an integer, and a function `g' statically declared to take
an *even* integer, then a static type-checker would reject `g(f())' as possibly
incorrect. (Assuming of course that such things were part of the type system.)
I am thinking of "optimistic" or "cheerful" static type-checkers which accept
code that is of uncertain safety, while rejecting code that is statically proven
to be incorrect. For example, a cheerful type-checker would accept `g(f())'
(possibly while emitting a warning), but if function `h' accepts only odd-
integer arguments, then it would reject `h(f())'.
I know that the Beta language  does this for object types. That is: if it
cannot statically prove that an operation is typesafe, then it inserts a run-
time check. I also know that C++ and Java programmers gain this same effect by
using their language's run-time downcast operator in specific places.
The reason I am thinking of this is that a pessimistic static type system can
constrain the programmer from writing code which *would* actually be correct,
although the type-checker can't prove it, where a cheerful static type system
would err on the other side, statically allowing code (hopefully with Beta-
style run-time checks) which is actually incorrect. This latter approach seems
more "lightweight" to me.
If anyone knows of an analysis of this notion I would appreciate a reference to
it. Also, I would be interested in your opinions about whether such "cheerful"
static type-checker (hopefully in combination with type-inference) would be
useful without incurring the "heavyweight" quality of typical static typing.
Security and Distributed Systems Engineering