3 ms·
It is also interesting to consider the PL definition of type safety: the progress and preservation theorems. Progress: if an expression is well typed then eith
by emillon 12y ago
It is also interesting to consider the PL definition of type safety: the progress and preservation theorems.
Progress: if an expression is well typed then either it is a value, or it can be further evaluated (in the sense that "an appropriate evaluation rule exists").
Preservation: if an expression e has type t, and is evaluated to e', then e' has type t.
That's it, really (well, you can do a few extensions to allow errors such as division by zero, or take memory into account).
If your language has both of these properties, they tell you that typed expressions will behave nicely at run time.
- tel 12y agoThat's it for the definition, but it's far from it for the meaning. Python/Ruby make a great example when they're interpreted as vacuously type safe—clearly this definition needs other components in order to be meaningful. And that's really the rub. You want a language which is type safe and possessing expressive types. Getting both is challenging.
- emillon 12y agoIndeed. In dynamically typed, every expression is well typed and there is always an evaluation rule that works, so this trivially holds but means nothing.
- mnarayan01 12y agoSaying that e.g. Ruby is "vacuously type safe" strikes me as fairly misleading. Consider an extension to Ruby which defines the ++ operator as casting its argument as an integer (e.g. Fixnum) and incrementing it. "Properly" defined, this operator would break type safety in a way that __can not__ currently be done in Ruby (i.e. modifying a string from "abcdefgh" to "bbcedefgh", "abcdefgi", or some other nonsense). This is clearly a type error, and it is one that Ruby does not allow, so describing Ruby's type _safety_ as vacuous strikes me as wrong. Additionally, Ruby prevents e.g. calling on an undefined method on an object. Given the way the interpreter works this comes trivially, but that does not mean that it does not affect type safety. To summarize: there are certain classes of type errors related to e.g. casting which would be dumb to allow in a (non-toy) dynamically typed language and others which come with no particular cost. This does not mean the type safety of the language is "vacuous" (though it may negate the need for an explicit "type checker").
- tel 12y agoWhat you're referring to may be both (a) true and (b) valuable but simply isn't "type safety" as is being discussed. It's unfortunately confusing to talk about this stuff since "type" is an overloaded word.