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

[address@hidden]

Zooko <zooko@zooko.com> writes:

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

This is what I meant by having to address the definition of
`checking'.  I'm sure that someone in the static type camp would
suggest that you need *not* refuse to execute a program that the type
checker could not prove correct.  (I'm equally sure that someone in
the static type checking camp will suggest that such a thing may not
technically a program!)