[Types-sig] type-asserts and check/run -time (was: updated proposal)

Tim Peters tim_one@email.msn.com
Wed, 5 Jan 2000 20:30:30 -0500

[Greg Stein]
> ...
> You and I know what that code says. Why should we state that
> the type-checker can never be as smart as us? The whole
> *point* of the type-checker is for it to be smarter than we
> are. We are trying to use it to find the places where we are
> being stupid.

Actually, that's what you're trying to use it for.  I maintain that most
people who want static typing are going to wag their heads in bewilderment
at anything fancier (or muddier) than a traditional "declare it or die"
system of purely compile-time annotations.

An interesting contrast is the recent Mercury language, basically Prolog on
hyperspeed steroids:


Their inferencers (plural because Prolog has stuff beyond types that needs
to be guessed -- e.g., whether a clause "generates" exactly one, no more
than one, or any number of results) are quite capable, but are used only to
verify the user's explicit declarations.  Everything must be declared.
Prolog is such that it's not hard to construct programs for which inference
is impossible; Mercury's response in such cases is to reject the program at
compile-time (i.e., if they can't prove your declarations are correct, you
lose, case closed, no appeal to the slower runtime court).

Mercury's concerns are industrial-strength safety and industrial-strength
speed, and their rigid declaration rules are what that crowd expects:  they
don't want "help", they want absolute compile-time guarantees.

Anyway, I'm not fighting this one way or the other anymore -- if you're
writing the code, you win <wink>.  I'll whine about it later -- provided
there's actually whineworthy behavior.

more-code-less-talk-ly y'rs  - tim