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

[Zooko <address@hidden>]

Greetings, ll1-discuss!

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 [1] 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.


Thanks!

Regards,

Zooko

[1] http://www.daimi.au.dk/~beta/Papers/BetaOverview/betaoverview.abstract.html

---
                 zooko.com
Security and Distributed Systems Engineering
---