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